MIPT-Coq-24-Lect-14

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: верификация алгоритма сортировки вставками, реализованного в Coq'е (продолжение); определение императивного ЯП и его семантики; представление состояний частичными функциями; синтаксис и семантика арифметических и булевозначных термов, функциональный и реляционный варианты; синтаксис и семантика управляющих конструкций.

Видео MIPT-Coq-24-Lect-14 автора evgeny.dashkov