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.
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.
