Mission : Le projet a pour objet de participer au développement d'extensions de la théorie équationnelle de l'assistant à la preuve Rocq, en lien avec la théorie des types cubiques et des outils de la réécriture. Le candidat mettra en œuvre ses connaissances et compétences en théorie des types, formalisation des mathématiques et programmation fonctionnelle. Activités : - Mise en place d'outils de réécriture modulo dédiés au sein de l'écosystème Rocq - Intégration de ces outils de réécriture à la théorie des types dépendants - Formalisation en Rocq de modules de théorie des types cubiques - Comparaison entre formalisation cubique et simplicial de l'axiome d'univalente - Etude bibliographique et comparaisons entre différentes approches logicielles - Organisation d'ateliers / de conférences. - Publication d'un compte-rendu final.