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.
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
Chercheur

Valery Isaev
Chercheur

Fedor Part
Chercheur

Alexander Kuklev
Chercheur

Marat Khabibullin
Développeur de logiciels