JetBrains Research — наука, меняющая мир

Семинар: Метод прогрессивной элиминации

Система Coq является мощным инструментом для программирования в терминах

зависимых типов данных. Возможности автоматизация построения

доказательств с использованием языка тактик способствовали широкому

распространению Coq в качестве proof assistant; вместе с тем попытки

оседлать мощную систему типов Coq для собственно написания программ

часто наталкиваются на проблемы. В частности, трудности возникают при

элиминации данных глубоко-зависимых типов, например, с использованием

тактик destruct/inversion, а также сопоставления с образцом. В докладе

будут рассмотрены некоторые из таких трудностей и способы их разрешения.


Докладчик: Дмитрий Булычев

02.11.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 2