Исследовательская группа
Лаборатория языковых инструментов
Канонические структуры в Coq
November 11
Механизм канонических структур в Coq позволяет верификатору управлять выводом типов, имитировать классы типов, синтезировать доказательства. Программируемый вывод типов является одним из ключевых архитектурных решений для формализации теоремы Фейта-Томпсона и широко используется в библиотеке Mathcomp.
На основе конкретных примеров мы рассмотрим механизм работы унификации в Coq, коснёмся вопросов построения иерархии математических (алгебраических) структур, а также сравним между собой различные механизмами вывода неявных аргументов, включая канонические структуры, классы типов и подсказки унификации.
Докладчик: Антон Трунов