MIPT-Coq-26-Lect-05

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