HoTT and Dependent Types Lab

В настоящее время группа работает над созданием формального языка с зависимыми типами, основанного на гомотопической теории типов (homotopy type theory, сокращенно — HoTT). Глобальная цель исследовательской группы заключается в том, чтобы разработать на базе современной теории типов многопользовательскую онлайн-систему верификации доказательств, пригодную для формализации отдельных разделов математики.

Идея проекта возникла в 2012 году, когда одна из команд JetBrains занималась совместным онлайн-редактором, основанным на операционных преобразованиях. Соответствующий алгоритм удалось разработать и верифицировать с помощью системы доказательства теорем Coq, а интерес к прикладным аспектам формальной верификации и автоматической проверки доказательств привел к созданию отдельной исследовательской группы. В 2015 году она переключилась на разработку экспериментального языка на основе HoTT.

Официальный сайт проекта

Состав

Сергей Синчук
Исследователь
Валерий Исаев
Исследователь
Фёдор Парт
Исследователь