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