Groupe de recherche

Groupe HoTT et types dépendants

Le groupe travaille actuellement à la création d’un langage dactylographié à typage dépendant basé sur la théorie des types homotopiques (HoTT). Le but ultime du projet est de créer un assistant de preuve collaboratif en ligne basé sur une théorie de type moderne pour permettre la formalisation de certaines branches des mathématiques.

Le projet a débuté en 2012 lorsque l’une des équipes de JetBrains a développé un éditeur collaboratif en temps réel basé sur la transformation opérationnelle (OT). Avec l’aide de l’assistant de preuve Coq, un algorithme OT approprié a été développé et validé, mais l’intérêt pour la vérification automatisée des preuves et la vérification formelle appliquée à des tâches réelles a conduit à la création d’un groupe de recherche distinct. En 2015, le groupe est passé au développement du langage expérimental HoTT.

Site officiel

Articles sur Arend (en russe) :

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

Membres du groupe

Sergey Sinchuk
Sergey Sinchuk
Chercheur
Valery Isaev
Valery Isaev
Chercheur
Fedor Part
Fedor Part
Chercheur
Alexander Kuklev
Alexander Kuklev
Chercheur
Tesla Zhang
Tesla Zhang
Chercheur