1. Семантика и её значение
2. Введение в Coq
3. Семантика большого шага для императивного языка
4. Множественные цели в Coq. Д-во корректности Constant Folding
5. Coq. Разбор д-ва терминируемости алгоритма Евклида
6. Семантика малого шага, логика Хоара
7. Coq. Семантика малого шага, логика Х