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\, University of Bath
DTSTART:20110506T130000Z
DTEND:20110506T140000Z
UID:TALK30617@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:We investigate the problem of type isomorphisms in a programmi
 ng language with higher-order references. We first recall the game-theoret
 ic model of higher-order references by Abramsky\, Honda and McCusker. Solv
 ing an open problem by Laurent\, we show that two finitely branching arena
 s are isomorphic if and only if they are geometrically the same\, up to re
 naming of moves (Laurent's forest isomorphism). We deduce from this an equ
 ational theory characterising isomorphisms of types in a finitary language
  L_2 with higher order references. We show however that Laurent's conjectu
 re does not hold on infinitely branching arenas\, yielding a non-trivial t
 ype isomorphism in the extension of L_2 with natural numbers. 
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR