University of Cambridge > Talks.cam > Category Theory Seminar >  Isomorphisms of types in the presence of higher-order references

Isomorphisms of types in the presence of higher-order references

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity