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