Qu'est ce que la théorie homotopique des types? Conférence d'André Joyal, docteur d'honneur 2017 de la Faculté des sciences
- Date :
- Cet événement est passé.
- Type :
- Conférences et séminaires
- Public :
- Membres de la communauté universitaire
- Lieu :
- Faculté des sciencesLocal : D4-2019
- Coût :
- Gratuit
Description :
Résumé: La théorie des types de Matrin-Löf est un langage formel pour les mathématiques constructives et la programmation. Il est au coeur du système Coq pour l'écriture de preuves formelles vérifiées par ordinateur. Une interprétation homotopique du language a été trouvée by Awodey et Warren et indépendamment par Voevodsky. Cette découverte permet d'envisager une axiomatisation complète de la théorie de l'homotopie à partir de principes simples. Je vais esquisser les règles de la théorie des types, décrire l'interprétation homotopique et l'axiome d'univalence e Voevodsky. Je parlerai de mes travaux si le temps le permet.