Colloque - Formalisation des mathématiques et types dépendants - Assia Mahboubi : Preuves formelles mutatis mutandis
Description
Collège de France
Thierry Coquand
Informatique et sciences numériques (2024-2025)
Année 2024-2025
Colloque - Formalisation des mathématiques et types dépendants - Assia Mahboubi : Preuves formelles mutatis mutandis
Assia Mahboubi
Directrice de recherche, Inria
Ré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 Mahboubi
Assia 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.
United States
