MIPT-Coq-CyPr-23-Lect-02

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