Contextual Isomorphisms

Add to your list(s) Download to your calendar using vCal

• Paul Levy (University of Birmingham)
• Friday 21 November 2014, 12:00-13:00
• CS 217.

If you have a question about this talk, please contact Neel Krishnaswami.

What is the right notion of “isomorphism” between types, in a simple type theory? The conventional answer is: two terms that are inverse up to contextual equivalence. I will argue that, in the presence of effects, this is too weak. I will propose instead a notion of “contextual isomorphism” that works both for call-by-value (or value types) and for call-by-name (or computation types). In the absence of effects it is equivalent to the conventional notion.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 217
• Lab Lunch

Note that ex-directory lists are not shown.