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

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

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

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

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

Официальный сайт проекта: https://arend-lang.github.io/

Статьи о языке Arend:

https://habr.com/ru/company/JetBrains-education/blog/469569/

https://habr.com/ru/company/JetBrains-education/blog/470632/

Новости

Публикации