01 – Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de Bruijn

Collège de FranceThierry CoquandInformatique et sciences numériques (2024-2025)Année 2024-202501 - Théorie des types dépendants et formalisation des mathématiques : La théorie des types, de Russell à de BruijnPlan 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 AUTOMATH ; traitement uniforme des objets et des preuves mathématiques ; vérification des preuves comme vérification des types.