MIPT-Coq-26-Lect-04

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