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

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202504 - Théorie des types dépendants et formalisation des mathématiques : Théorie des types et théorie des ensemblesPlan 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).