03 - Théorie des types dépendants et formalisation des mathématiques : Univers, paradoxes et normalisation
Update: 2025-03-31
Description
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.
Comments
In Channel