Martin-Löf, Constructive mathematics and computer programming.
Организатор: @orenty7
Изоморфизм Карри-Ховарда — краеугольный камень современных систем проверки доказательств. Как оказалось, логики и теории типов это две стороны одной монеты: аффинные типы (Rust) соответствуют аффинным логикам, System F (Haskell) соответствует конструктивной логике высказываний второго порядка, а MLTT (Agda) и CIC (Rocq/Lean) — конструктивным логикам предикатов высших порядков. Последние две нам особенно интересны, ведь именно в них активно развиваются формально верифицированные математика и computer science. Данная статья — обзор основных идей MLTT от самого создателя.
Прочитать статью к воскресенью, 14 июня. Встречаемся на нашем дискорд-сервере в 20:00 по Москве.
Статья в первом комменте.
Формат | Методы доступа в дискорд
Организатор: @orenty7
Изоморфизм Карри-Ховарда — краеугольный камень современных систем проверки доказательств. Как оказалось, логики и теории типов это две стороны одной монеты: аффинные типы (Rust) соответствуют аффинным логикам, System F (Haskell) соответствует конструктивной логике высказываний второго порядка, а MLTT (Agda) и CIC (Rocq/Lean) — конструктивным логикам предикатов высших порядков. Последние две нам особенно интересны, ведь именно в них активно развиваются формально верифицированные математика и computer science. Данная статья — обзор основных идей MLTT от самого создателя.
Прочитать статью к воскресенью, 14 июня. Встречаемся на нашем дискорд-сервере в 20:00 по Москве.
Статья в первом комменте.
Формат | Методы доступа в дискорд