Date(s) : 11/12/2014 iCal
14 h 00 min - 15 h 00 min
Je présenterai des travaux en cours (en collaboration avec Dan Licata) sur le développement d’une théorie des types cubique, le but étant d’obtenir une théorie des types ayant de bonnes propriétés calculatoires (normalisation forte, canonicité, décidabilité du typage) tout en étant compatible avec la théorie des types homotopiques, en particulier avec l’axiome d’univalence et les types inductifs supérieurs. Ces travaux sont égalements très liés aux travaux de Thierry Coquand, Simon Huber et Marc Bézem sur un modèle constructif de la théorie des types homotopiques dans les ensembles cubiques.
[http://math.unice.fr/laboratoire/fiche&id=556]
Catégories Pas de Catégories