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

Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 Colloque - Formalisation des mathématiques et types dépendants - Denis-Charles Cisinski : La logique des catégories supérieures Denis-Charles Cisinski Professeur, Universität Regensburg Résumé La logique des catégories supérieures (ou encore des ∞-catégories) est une variation de la théorie des types...

Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-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 Maî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 de...

Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 Colloque - Formalisation des mathématiques et types dépendants - Pierre-Marie Pédrot : Pour s'asseoir sur les fondations Pierre-Marie Pédrot Chargé de recherche, Inria Ré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'informa...

Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 Colloque - Formalisation des mathématiques et types dépendants - Assia Mahboubi : Preuves formelles mutatis mutandis Assia Mahboubi Directrice de recherche, Inria Ré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 l...

Collège de France Thierry Coquand Informatique et sciences numériques (2024-2025) Année 2024-2025 Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances divisées Antoine Chambert-Loir Professeur, 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...

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

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

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

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

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

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

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

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

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