BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY: Isomorphisms of types in the presence of higher-order references 
 - Pierre Clairambault\, Cambridge
DTSTART:20120221T141500Z
DTEND:20120221T151500Z
UID:TALK34888@talks.cam.ac.uk
CONTACT:Julia Goedecke
DESCRIPTION:Just as in category theory\, the natural notion of equivalence
  between types of a programming language is not syntactical equality but i
 somorphism: isomorphisms of types have turned out to be important as tools
  for a modular approach of programming. Consequently they have been studie
 d in simply typed lambda calculus (isomorphisms of the free CCC) but also 
 in several of its extensions\, for instance with coproducts\, polymorphism
 s\, etc. They are now used routinely in several tools for managing librari
 es in functional programming languages such as ML. However\, these\nlangua
 ges are not purely functional: they usually feature imperative effects suc
 h as the use of state\, and the previous results on isomorphisms do not ta
 ke these into account. In 2005\, it was conjectured by Laurent that refere
 nces do not change the theory of isomorphisms of types. In this talk I wil
 l present my recent work on this issue. Applying ideas from game semantics
  I will describe a proof of Laurent's conjecture when the types\nare finit
 ary\, i.e. without natural numbers. Unexpectedly\, Laurent's conjecture tu
 rns 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-or
 der store. 
LOCATION:MR5\, Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR