Лаборатория языковых инструментов

Система Coq является мощным инструментом для программирования в терминах зависимых типов данных. Возможности автоматизация построения доказательств с использованием языка тактик способствовали широкому распространению Coq в качестве proof assistant; вместе с тем попытки оседлать мощную систему типов Coq для собственно написания программ часто наталкиваются на проблемы. В частности, трудности возникают при элиминации данных глубоко-зависимых типов, например, с использованием тактик destruct/inversion, а также сопоставления с образцом. В докладе будут рассмотрены некоторые из таких трудностей и способы их разрешения.

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