Isomorphisms of types in the presence of higher-order references

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

• Pierre Clairambault, Cambridge
• Tuesday 21 February 2012, 14:15-15:15
• MR5, Centre for Mathematical Sciences.

If you have a question about this talk, please contact Julia Goedecke.

Just as in category theory, the natural notion of equivalence between types of a programming language is not syntactical equality but isomorphism: isomorphisms of types have turned out to be important as tools for a modular approach of programming. Consequently they have been studied in simply typed lambda calculus (isomorphisms of the free CCC ) but also in several of its extensions, for instance with coproducts, polymorphisms, etc. They are now used routinely in several tools for managing libraries in functional programming languages such as ML. However, these languages are not purely functional: they usually feature imperative effects such as the use of state, and the previous results on isomorphisms do not take these into account. In 2005, it was conjectured by Laurent that references do not change the theory of isomorphisms of types. In this talk I will present my recent work on this issue. Applying ideas from game semantics I will describe a proof of Laurent’s conjecture when the types are finitary, i.e. without natural numbers. Unexpectedly, Laurent’s conjecture turns out to be false in general, and I will present some new isomorphisms of types that appear with the combination of natural numbers and higher-order store.

This talk is part of the Category Theory Seminar series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Category Theory Seminar
• DPMMS Lists
• DPMMS Pure Maths Seminar
• DPMMS info aggregator
• DPMMS lists
• Hanchen DaDaDash
• Interested Talks
• MR5, Centre for Mathematical Sciences
• School of Physical Sciences
• bld31
• ndb35's list
• yk373's list

Note that ex-directory lists are not shown.