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

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.