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 FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202508 - Théorie des types dépendants et formalisation des mathématiques : Modalités et modèles de la théorie des typesPlan 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.