03 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisation
Épisode de Informatique et sciences numériques (2024-2025) - Thierry Coquand par Collège de France · 31 mars 2025 · 1 h 13 min
Collège de France
Thierry Coquand
Informatique et sciences numériques (2024-2025)
Année 2024-2025
03 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisation
Plan 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 collage à la Artin et preuve de normalisation ;
application à la vérification des preuves.
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 - Assia Mahboubi : Preuves formelles mutatis mutandis 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
- 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
À 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
- 2026-04 V2 PINS.mp4 – Lille.Pod
- Episode #16 Jordan Marion - L'école d'astrologie – Pour l’Amour du Ciel
- E116 - Why You Understand French but Can't Speak It – Intermediate French Podcast - Ta vie en français
- La guillotine : un progrès social ? # Révolution française 🇫🇷 DELF A2 / B1 - French intermediate level - Compréhension orale – Escargot - News & Culture in Simple French
- André Malraux – La base
- (133) L’amour ne suffit pas ! Comment bien se disputer en couple (avec Sandy Kaufmann) – J'ai peur, donc j'y vais
Tous les épisodes de Informatique et sciences numériques (2024-2025) - Thierry Coquand · Plus de podcasts Éducation