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

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

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 et la nécessité de lui octroyer une place pleine et entière. Théorie des types dépendants et formalisation des mathématiques 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 types dépendants présente aussi un intérêt conceptuel intrinsèque en logique et informatique, à travers la correspondance de Curry-Howard entre types et propositions. De plus, Voevodsky a pu donner à la notion de type dépendant une sémantique naturelle en théorie abstraite de l'homotopie, et ce rapprochement inattendu entre des questions de base de la logique et de la théorie de l'homotopie apparaît fondamental. Le cours que nous proposons pour l'année 2024–2025 s'inscrit dans ce foisonnement d'idées autour des théories des types. Dans la première partie, on présentera en détail la théorie des types dépendants et ces propriétés métamathématiques qui justifient son utilisation pour la vérification des preuves sur ordinateur. La deuxième partie du cours sera consacrée à la synergie qui est en train de s'établir entre cette théorie et la théorie de l'homotopie. Biographie Après des études à l'École normale supérieure de Paris, Thierry Coquand passe sa thèse d'informatique théorique en 1985, introduisant la théorie des constructions, formalisme utilisé dans plusieurs systèmes d'assistants à la démonstration. Depuis 1996, il est professeur en informatique à l'université de Göteborg, en Suède. Ses recherches concernent les mathématiques constructives, la théorie des types et ses applications pour la représentation des preuves sur ordinateur, et la sémantique des langages de programmation. Il a été coorganisateur, avec Vladimir Voevodsky et Steve Awodey, de l'année spéciale 2012-2013 à l'Institute of Advanced Study, Princeton, sur les Univalent Foundations of Mathematics. Ses travaux récents ont pour but de donner un sens effectif à l'axiome d'univalence, introduit par Voevodsky, et aux modèles de faisceaux (topos d'ordre supérieur). Pour ses travaux en logique, il a eu le Kurt Godel Centenary Research Prize 2008, et pour ses travaux sur les assistants de preuve, il a reçu, en collaboration, le ACM SIGPLAN Programming Languages Software Award, 2013.

Publisher

Collège de France

Category

education

Language

fr

Explicit

No

First episode

13 Mar 2025

Latest episode

2 Jun 2025

Latest episodes

14 episodes in the feed.

1. 

   2 Jun 2025

   Colloque - Formalisation des mathématiques et types dépendants - Denis-Charles Cisinski : La logique des catégories supérieures

   Professor Denis-Charles Cisinski discusses the logic of higher categories, a variation of type theory that is homotopical, and its potential to provide a foundation for mathematics where category theory and homotopy theory are implemented in this interview.

2. 

   2 Jun 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

   Riccardo Brasca, lecturer at Université Paris Cité, presents recent progress in formalizing number theory within Lean's mathlib, highlighting advancements and future implications for formalized mathematics; this is a lecture.

3. 

   2 Jun 2025

   Colloque - Formalisation des mathématiques et types dépendants - Pierre-Marie Pédrot : Pour s'asseoir sur les fondations

   Pierre-Marie Pédrot discusses the formalization of mathematics and dependent types, focusing on the computer science perspective and the proof-program equivalence, in this interview with Thierry Coquand.

4. 

   2 Jun 2025

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

   Assia Mahboubi, Inria Research Director, presents formal proof transfer tools applicable in proof assistants like Rocq or Lean when adding mathematical concepts to formal libraries, in this interview.

5. 

   2 Jun 2025

   Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances divisées

   Antoine Chambert-Loir discusses the formalization of divided powers, an algebraic tool crucial for constructing crystalline cohomology, and its applications in algebraic topology within mathematics.

6. 

   19 May 2025

   08 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des types

   Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 08 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des types Plan 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 de modèle de Quillen et modèle constructif de la notion de types d'homotopie.

7. 

   12 May 2025

   07 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologie

   Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 07 - Théorie des types dépendants et formalisation des mathématiques : Espaces d'Eilenberg-MacLane et cohomologie Plan 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 pour définir les groupes de cohomologie.

8. 

   5 May 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

   Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-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 Plan 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 de structure de modèle la Quillen sur certains modèles de préfaisceaux ; définition constructive des types d'homotopie des espaces topologiques.

9. 

   28 Apr 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

   Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-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 Plan 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 notion d'équivalence ; principe d'univalence ; application à la notion d'égalité des structures mathématiques et comparaison avec la théorie des ensembles.

10. 

    7 Apr 2025

    04 - Théorie des types dépendants et formalisation des mathématiques : Théorie des types et théorie des ensembles

    Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 04 - Théorie des types dépendants et formalisation des mathématiques : Théorie des types et théorie des ensembles Plan 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 logique de certains systèmes de types et en particulier du système Lean (Mario Carneiro).

11. 

    31 Mar 2025

    03 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisation

    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.

12. 

    24 Mar 2025

    02 - Théorie des types dépendants et formalisation des mathématiques : Déduction naturelle et modèles

    Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 02 - Théorie des types dépendants et formalisation des mathématiques : Déduction naturelle et modèles Plan 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 ; quelques exemples de modèles, en particulier modèle ensembliste et modèles de préfaisceaux.

13. 

    17 Mar 2025

    01 - Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de Bruijn

    Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 01 - Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de Bruijn Plan 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 ; traitement uniforme des objets et des preuves mathématiques ; vérification des preuves comme vérification des types.

14. 

    13 Mar 2025

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

    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.

Who has been a guest on Informatique et sciences numériques (2024-2025) - Thierry Coquand

Names identified in recent episode analyses. Showing up to five guests.

• Denis-Charles Cisinski
• Riccardo Brasca
• Pierre-Marie Pédrot
• Assia Mahboubi
• Antoine Chambert-Loir