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

Материалы в репозитории: https://github.com/anton-trunov/csclub-coq-course-spring-2021