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

Épisode de Informatique et sciences numériques (2024-2025) - Thierry Coquand par Collège de France · 2 juin 2025 · 50 min

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.

Autres épisodes de « Informatique et sciences numériques (2024-2025) - Thierry Coquand »

• Colloque - Formalisation des mathématiques et types dépendants - Denis-Charles Cisinski : La logique des catégories supérieures 2 juin 2025
• Colloque - Formalisation des mathématiques et types dépendants - Riccardo Brasca : Progrès récents dans la formalisation de la théorie des nombres 2 juin 2025
• Colloque - Formalisation des mathématiques et types dépendants - Pierre-Marie Pédrot : Pour s'asseoir sur les fondations 2 juin 2025
• Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances divisées 2 juin 2025
• 08 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des types 19 mai 2025
• 07 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologie 12 mai 2025
• 06 - Théorie des types dépendants et formalisation des mathématiques : Modèles de la théorie des types et du principe d'univalence 5 mai 2025
• 05 - Théorie des types dépendants et formalisation des mathématiques : Le mystère de l'égalité ; la notion de type comme généralisation de la notion d'ensemble 28 avril 2025
• 04 - Théorie des types dépendants et formalisation des mathématiques : Théorie des types et théorie des ensembles 7 avril 2025
• 03 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisation 31 mars 2025
• 02 - Théorie des types dépendants et formalisation des mathématiques : Déduction naturelle et modèles 24 mars 2025
• 01 - Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de Bruijn 17 mars 2025
• Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstration 13 mars 2025

Tous les épisodes de Informatique et sciences numériques (2024-2025) - Thierry Coquand · Plus de podcasts Éducation