MIPT-Coq-25-Lect-05

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