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

Семинар: Канонические структуры в Coq

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

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

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

11.11.2019, 17:15.

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