Type theory modulo isomorphisms

Alejandro Díaz-Caro
INRIA Rocquencourt & Paris Ouest

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

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.



Retour en haut 

Secured By miniOrange