О чем курс

В круг тем, охватываемых данным предметом, входят подходы к точному описанию семантики языковых конструкций и методам доказательства корректности преобразований программ.

• Операционная семантика малого и большого шага императивного языка программирования,

• Денотационная семантика,

• Аксиоматическая семантика Хоара,

• Семантика языков с многопоточностью,

• Слабые модели памяти.

Пререквизиты к курсу

Функциональное программирование

Желательно: Математическая логика

Что студенты будут уметь после окончания курса

После успешного прохождения курса слушатель:

• Знает основные стили семантик языков программирования: денотационный, операционный, аксиоматический; композиционность. Умеет аргументированно описать выбранный стиль и преимущества его использования для конкретной задачи.

• Знает эквивалентность программ и семантик. Знает варианты определений и их взаимоотношения, обоснование свойств преобразований программ.

• Знает понятие операционной семантики. Умеет получать и анализировать дерево вывода программы. Владеет навыками использования семантики большого и малого шагов.

• Обладает базовыми навыками работы с системой интерактивного доказательства теорем Coq. Умеет формализовывать различные семантики и доказательства их свойств в Coq, а также верифицировать программы с помощью логики Хоара.

Критерии оценивания

Оценка за курс будет в равной степени состоять из результата выполнения практических заданий в течение курса, а также двух устных экзаменов в середине и в конце курса.

Максимум за курс 10 баллов:

• 4 балла за домашние задания (на языке Coq);

• 2 балла за устный экзамен №1;

• 2 балла за устный экзамен №2;

• 2 балла за активность на занятиях.

Что нужно иметь с собой на занятиях

Будет нужен компьютер с установленным Coq и средой для редактирования (см. ниже).

Установка Coq и нужных библиотек

С помощью opam нужно установить библиотеки coq>=8.9.1, bignums и hahn:

opam remote add coq-released https://coq.inria.fr/opam/released
opam remote add coq-weakmemory-local -k git https://github.com/weakmemory/local-coq-opam-archive
opam install coq coq-bignums coq-hahn

Среда для редактирования Coq

Coq предполагает интерактивное взаимодействие, поэтому понадобится или специальный редактор (CoqIDE), или плагин для вашего любимого текстового редактора (ProofGeneral для Emacs, VsCoq для VSCode). Для Vim тоже есть, но рекомендовать не могу -- использовал давно.

Мы используем Emacs (+ Evil mode для эмуляции Vim в Emacs).

Виртуальная машина

Виртуальная машина (Ubuntu 18.04) с установленным Coq 8.9.1, необходимыми библиотеками и IDE доступна по здесь. Логин/пароль semantics.

Практические задания

Задания находятся здесь.

Литература

• Glynn Winskel. The Formal Semantics of Programming Languages;
• Coq tactics cheatsheets (краткая информация по тактикам): Link 1, Link 2
• Полная информация по тактикам: Coq Reference Manual;
• Классический вводный курс по Coq: Software Foundations. Logical Foundations.

Родственные курсы

• Основы формальной верификации

На нашем курсе про Coq будет рассказан необходимый минимум для задачек, которые будут рассматриваться на семинаре, и Coq будет в первую очередь инструментом для доказательства свойств семантик. В курсе Основы формальной верификации будет более подробный рассказ про Coq. Также, в нашем курсе будет использоваться стандартный Coq, тогда как в Основы формальной верификации -- Coq в связке с библиотекой MathComp, что подразумевает немного другой стиль.