MIPT-Coq-24-Lect-04

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: программирование в лямбда-исчислении с простыми типами; типы как пропозициональные формулы; населенные типы и тавтологии; система натурального вывода (для импликативного фрагмента) и ее связь с выводом типов.