MIPT-Coq-24-Lect-04

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

0/0


0/0

0/0

0/0