Введение в курс, основы функционального программирования в Coq

Введение в курс: формальные методы в целом, интерактивное доказательство теорем в частности. Практическая применимость. Выдающиеся проекты в области формальных методов. Основы тотального функционального программирования в Coq: синтаксис Gallina, интерактивные запросы в Coq.