MIPT-Coq-25-Lect-02

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: термы и редукции в бестиповом лямбда-исчислении; теорема Чёрча-Россера; нормальные формы; представление булевых функций термами.