Le thème du colloque sera « Formalisation des mathématiques et types dépendants ». Les invités du colloque sont des spécialistes de l’implémentation ou de la théorie des assistants de preuve, de la théorie des types, des notions de catégorie d’ordre supérieur, et des mathématiciens qui utilisent ces systèmes pour représenter les preuves sur ordinateur. Une des questions abordées sera dans quelle mesure le rapprochement récent entre le formalisme des types dépendants et les notions d’homotopie et de catégories d’ordre supérieur peut être pertinent pour la formalisation effective des mathématiques.
Colloque