Séminaires


Retour à la liste de tous les séminaires


Interprétation catégorique cohérente de la théorie des types

Le : 01/12/2015 14h00
Par : Pierre-Louis Curien (équipe pi.r2, laboratoire PPS, CNRS, Université Paris-Diderot et INRIA)
Lieu : I 103
Lien web :
Résumé : Une interprétation de la théorie (extensionnelle) des types de Martin-Löf dans les catégories localement cartésiennes fermées a été proposée au début des années 80 par Seely. Cette interprétation ne prenait pas en compte d’importantes considérations de cohérence, dues au fait que la syntaxe de la théorie des types gère l’associativité de la substitution de manière exacte alors que le modèle catégorique ne la modélise qu’à iso près. Indépendamment, Curien et Hofmann, dans les années 90, ont proposé deux solutions indépendantes et distinctes à ce "mismatch", et dans un travail de 2012, Curien, Garner et Hofmann replacent ces deux solutions dans un cadre commun. Ce cadre s’applique aussi à la théorie des types intensionnelle.