Type theory modulo isomorphisms
Alejandro Díaz-Caro
INRIA Rocquencourt & Paris Ouest
https://www-2.dc.uba.ar/staff/adiazcaro/
Date(s) : 09/04/2014 iCal
14h00 - 15h00
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/
Catégories
