Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstration

Épisode de Informatique et sciences numériques (2024-2025) - Thierry Coquand par Collège de France · 13 mars 2025 · 53 min

Collège de France

Thierry Coquand

Informatique et sciences numériques (2024-2025)

Année 2024-2025

Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstration

Résumé

La théorie des types a été introduite par Bertrand Russell pour éviter les paradoxes qui apparaissent en mathématique si l'on utilise de manière trop naïve la notion de collection d'objets. Cette notion de types a été raffinée par la notion de type dépendant, dans le but de représenter les preuves mathématiques sur ordinateur, et de pouvoir ainsi vérifier la correction de ces preuves. Cette idée d'utiliser ainsi l'ordinateur connaît depuis quelques années un grand développement (vérification de la preuve du théorème de l'ordre impair ou, plus récemment, d'un résultat non trivial de Peter Scholze). Indépendamment de ce rôle important pour la formalisation des preuves mathématiques, la notion de type dépendant présente un intérêt conceptuel intrinsèque en logique et informatique, à travers la correspondance de Curry-Howard entre types et propositions. Certains résultats plus récents indiquent que ce formalisme permet de formuler des propriétés nouvelles sur une des notions de base de la mathématique : la notion d'égalité, avec un rapprochement inattendu entre des questions de base de la logique et de la théorie abstraite de l'homotopie.

Cette leçon retracera l'histoire récente de ces découvertes, aussi bien autour de la vérification des preuves sur ordinateur que de la synergie qui est en train de s'établir entre la théorie des types dépendants et la théorie de l'homotopie.

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

À propos du podcast

Informatique et sciences numériques (2024-2025) Thierry Coquand Année 2024-2025 Chaire annuelle Présentation de la chaire Créée en partenariat avec Inria, la chaire annuelle Informatique et sciences numériques marque une volonté commune de faire valoir l'importance de cette discipline scientifique…

Informatique et sciences numériques (2024-2025) - Thierry Coquand

Épisodes similaires

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