MIPT-Coq-26-Lect-06

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