Особенности теории типов Coq, часть 1

Среда, 13 мая 2020

Онлайн, занятие в zoom

Приложенные файлы

lecture11_extra.v hw11.v

Описание

Нерелевантность доказательств
Непредикативность Prop, предикативность Type
Большая элиминация и закон исключенного третьего
Тотальность и завершаемость программ
Фундированные отношения, Acc предикат и оператор выбора
Правило строгой позитивности для индуктивных типов