Type theory modulo isomorphisms

Carte non disponible
Speaker Home page :
Speaker :
Speaker Affiliation :


Date(s) - 09/04/2014
14 h 00 min - 15 h 00 min

Catégories Pas de Catégories

We defined a typed lambda-calculus where the isomorphisms between types are raised to the level of an equality relation. To this end, an equivalence relation is settled at the term level. We provide a proof of strong normalisation modulo such an equivalence, which is a non-trivial adaptation of the reducibility method. This work opens several paths for future work, which I will try to detail in this talk.

https://who.rocq.inria.fr/Alejandro.Diaz-Caro/« >https://who.rocq.inria.fr/Alejandro.Diaz-Caro/

Retour en haut 

Secured By miniOrange