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

Механизм канонических структур в Coq позволяет верификатору управлять выводом типов, имитировать классы типов, синтезировать доказательства. Программируемый вывод типов является одним из ключевых архитектурных решений для формализации теоремы Фейта-Томпсона и широко используется в библиотеке Mathcomp.

На основе конкретных примеров мы рассмотрим механизм работы унификации в Coq, коснёмся вопросов построения иерархии математических (алгебраических) структур, а также сравним между собой различные механизмами вывода неявных аргументов, включая канонические структуры, классы типов и подсказки унификации.

Докладчик: Антон Трунов