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

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

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

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

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

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

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

Состав

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