MIPT-Coq-24-Lect-03

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: минимизация; теорема о представимости любой вычислимой функции; вторая теорема о неподвижной точке, теорема Скотта и неразрешимость бестипового лямбда-исчисления; лямбда-исчисление с простыми типами (по de Bruijn'у); примеры "вывода типов" и свойства этой системы выводов; первый взгляд на Coq. ВНИМАНИЕ: к сожалению, качество звука в данном видео довольно плохое; надеюсь, что в последующих записях этого изъяна не окажется.

Видео MIPT-Coq-24-Lect-03 автора evgeny.dashkov