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

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

Collège de France 14 Épisodes juin 2, 2025

Ce podcast présente les cours de la chaire annuelle Informatique et sciences numériques du Collège de France, créée en partenariat avec Inria. Thierry Coquand y explore la théorie des types dépendants et la formalisation des mathématiques, une approche qui permet de vérifier la correction des preuves mathématiques sur ordinateur. La série couvre les développements récents dans ce domaine, notamment la vérification de théorèmes majeurs comme celui de l'ordre impair.

Épisodes

Colloque - Formalisation des mathématiques et types dépendants - Denis-Charles Cisinski : La logique des catégories supérieures juin 2, 2025 44:10 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Colloque - Formalisation des mathématiques et types dépendants - Denis-Charles Cisinski : La logique des catégories supérieuresDenis-Charles CisinskiProfesseur, Universität RegensburgRésuméLa logique des catégories supérieures (ou encore des ∞-catégories) est une variation de la théorie des types qui est

Colloque - Formalisation des mathématiques et types dépendants - Riccardo Brasca : Progrès récents dans la formalisation de la théorie des nombres juin 2, 2025 47:28 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Colloque - Formalisation des mathématiques et types dépendants - Riccardo Brasca : Progrès récents dans la formalisation de la théorie des nombresRiccardo BrascaMaître de conférences, université Paris CitéRésuméDans cet exposé, nous discuterons de l'état actuel de la formalisation de la théorie des nombre

Colloque - Formalisation des mathématiques et types dépendants - Pierre-Marie Pédrot : Pour s'asseoir sur les fondations juin 2, 2025 46:57 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Colloque - Formalisation des mathématiques et types dépendants - Pierre-Marie Pédrot : Pour s'asseoir sur les fondationsPierre-Marie PédrotChargé de recherche, InriaRésuméLa preuve assistée par ordinateur séduit un public de plus en plus large. Jusque-là surreprésentée dans le domaine de l'informatique où

Colloque - Formalisation des mathématiques et types dépendants - Assia Mahboubi : Preuves formelles mutatis mutandis juin 2, 2025 49:53 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 à pl

Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances divisées juin 2, 2025 44:30 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances diviséesAntoine Chambert-LoirProfesseur, université Paris CitéRésuméJe ferai le point sur un travail de formalisation de la théorie des puissances divisées que je mène avec María-In

08 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des types mai 19, 2025 77:44 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202508 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des typesPlan du cours :modalités exactes à gauche ;application pour construire des nouveaux modèles de la théorie des types ;non prouvabilité de la thèse de Church et du choix dénombrable ;structure

07 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologie mai 12, 2025 71:26 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202507 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologiePlan du cours :opération de débouclage des groupes ;un exemple paradigmatique de définition de types qui ne sont pas des ensembles, les espaces d'Eilenberg-MacLane ;utilisation de ces types pou

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 mai 5, 2025 75:30 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202506 - Théorie des types dépendants et formalisation des mathématiques : Modèles de la théorie des types et du principe d'univalencePlan du cours :modèle de Voevodsky des ensembles simpliciaux et caractère non effectif de ces modèles ;modèles effectifs avec ensembles cubiques ;application à une définition d

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 avr. 28, 2025 70:57 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202505 - 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'ensemblePlan du cours :comment représenter la notion d'égalité en théorie des types ; stratification de Voevodsky des types ; une définition uniforme de la

04 - Théorie des types dépendants et formalisation des mathématiques : Théorie des types et théorie des ensembles avr. 7, 2025 79:06 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202504 - Théorie des types dépendants et formalisation des mathématiques : Théorie des types et théorie des ensemblesPlan du cours :traduction d'Aczel de la théorie des ensembles en théorie des types ; variation de Miquel pour les ensembles non nécessairement bien fondés ; application au problème de la force

03 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisation mars 31, 2025 73:27 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202503 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisationPlan du cours :paradoxe de Girard avec un type de tous les types ; différence avec le paradoxe de Russell ; univers comme principe de réflexion ; preuve algébrique de canonicité avec la technique du c

02 - Théorie des types dépendants et formalisation des mathématiques : Déduction naturelle et modèles mars 24, 2025 65:17 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202502 - Théorie des types dépendants et formalisation des mathématiques : Déduction naturelle et modèlesPlan du cours :Curry-Howard ; déduction naturelle de Gentzen ; définitions inductives suivant Martin-Löf ; présentation algébrique de la théorie des types et modèle des termes comme modèle initial ; quelqu

01 - Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de Bruijn mars 17, 2025 62:41 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202501 - Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de BruijnPlan du cours :théorie des types de Russell ;notation du λ-calcul de Church pour les fonctions ; théorie des types simples et système HOL ; introduction aux types dépendants, système AUTOMATH

Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstration mars 13, 2025 52:46 Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-2025Leçon inaugurale - Thierry Coquand : La théorie des types, de Russell aux assistants à la démonstrationRé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 n