Семантики языков программирования 3 модуль 2019

Материал из CSC Wiki
Перейти к:навигация, поиск

Преподаватель -- Подкопаев Антон Викторович, anton@podkopaev.net

Оценивание

Разбалловка по системе ВШЭ:

  • 4 балла за домашние задания (на языке Coq);
  • 4 балла за устный экзамен;
  • 2 балла за активность на занятиях.

Материалы курса

Рекомендуемая книга: The Formal Semantics of Programming Languages, Glynn Winskel

Ресурсы по Coq

Coq tactics cheatsheets (краткая информация по тактикам):

1) http://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf

2) https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html

Coq Reference Manual (полная информация по тактикам), https://coq.inria.fr/distrib/current/refman/

Software Foundations. Logical Foundations (классический "вводный" курс по Coq), https://softwarefoundations.cis.upenn.edu/lf-current/index.html

Примерные темы вопросов на экзамен

1. Семантика большого и малого шагов для выражений. Эквивалентность выражений. Индукция по дереву выражения. Детерминированность семантик.

2. Индукция. Фундированное множество.

3. Семантика большого и малого шагов для утверждений (statements). Детерминированность семантик. Параллельная композиция и её семантика.

4. Денотационная семантика. Мотивация. Денотационная семантика выражений. Монотонность и непрерывность операторов. Теорема о неподвижной точке непрерывного оператора.

5. Аксиоматическая семантика. Правила Хоара и их корректность.

6. Лямбда-исчисление. Простое типизированное лямбда-исчисление (STLC). Строгая и слабая нормализации. Теорема Чёрча-Россера. α- и β-эквивалентности. Семантики большого и малого шагов для CBN (call-by-name), CBV (call-by-value) и стандартного порядка редукций.

7. Слабые модели памяти. Последовательная консистентность (SC) и модель полного порядка на записях (TSO). Корректность компиляции из TSO в SC.