MIPT-Coq-CyPr-23-Lect-01

Введение в инженерию доказательств в МФТИ. Темы: (продолжение лекции по ФП) бестиповое лямбда-исчисление, редукции, теорема Чёрча-Россера.