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.