Colloque – Formalisation des mathématiques et types dépendants – Assia Mahboubi : Preuves formelles mutatis mutandis

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Colloque - Formalisation des mathématiques et types dépendants - Assia Mahboubi : Preuves formelles mutatis mutandisAssia MahboubiDirectrice de recherche, InriaRésuméComme c'est le cas dans la littérature, l'ajout d'un concept mathématique à un corpus de bibliothèques formelles donne typiquement lieu à plusieurs variantes de définitions, le plus souvent équivalentes mais pas toujours. Malheureusement, la transposition des preuves formelles de théorèmes associées à ces différentes variantes est alors très pédestre, alors que sur papier, ces étapes triviales resteraient implicites. Cette nécessaire bureaucratie est de fait un frein notoire à la formalisation de mathématiques « intéressantes ». Dans cet exposé nous discuterons la construction d'un outil de transfert de preuves en théorie des types. Base sur une généralisation de la traduction de paramétricité de Tabareau-Tanter-Sozeau, cette approche est utilisable dans des prouveurs comme Rocq ou Lean. Il s'agit d'un travail en collaboration avec Cyril Cohen et Enzo Crance.Assia MahboubiAssia Mahboubi est directrice de recherche à l'Inria, au sein du laboratoire des Sciences du Numérique de Nantes. Elle occupe aussi une chaire dans le département de mathématiques de la Vrije Universiteit Amsterdam, aux Pays-Bas.