Числення конструкцій
У травні 1986 року Тьєррі Кокан і Жерар Юе з INRIA випустили звіт про числення конструкцій — формалізм вищого порядку, у якому кожне доведення є лямбда-виразом, типізованим твердженням, яке воно доводить. Якщо стерти типи, лишається програма, що відповідає доведенню. Автори довели сильну нормалізацію: кожне обчислення завершується, а отже логіка несуперечлива.
Чому це важливо
Доведення й програма стали одним об'єктом, а перевірка доведення — перевіркою типу. Ядро Lean, за статтею його авторів, дає версію числення індуктивних конструкцій, що спирається на цю роботу; у Lean 2024–2026 років машина записує й перевіряє доведення олімпіадних задач і задач Ердеша.
Звіт спирається на відповідність Каррі — Говарда між твердженнями й типами і пише, що для інформатики з неї виходить функціональна мова дуже високого рівня, де тип може бути довільно складною специфікацією програми. Терми, за самими авторами, натхненні формалізмами Automath, з індексами де Брейна. У звіті немає виміру — це теорія, а не система. Зв'язок із Lean стоїть на статті його авторів 2015 року: ядро Lean може надати версію числення індуктивних конструкцій, з посиланням на Кокана і Юе. Чого запис не стверджує: коли вийшла перша версія Coq — прочитані документи цього не кажуть.