Исследовательская группа

Группа HoTT и зависимых типов

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

Глобальная цель исследовательской группы заключается в том, чтобы разработать на базе современной теории типов многопользовательскую онлайн-систему верификации доказательств, пригодную для формализации отдельных разделов математики.

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

Публикации