BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Marriage of Bisimulations and Kripke Logical Relations - Derek
  Dreyer\, MPI-SWS
DTSTART:20111101T150000Z
DTEND:20111101T160000Z
UID:TALK34319@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:There has been great progress in recent years on developing pr
 actical techniques for reasoning about program equivalence in ML-like lang
 uages---that is\, languages that combine features like higher-order functi
 ons\, recursive types\, abstract types\, and general mutable references. W
 hat has not emerged thus far is a clear understanding of how the different
  families of techniques relate to one another\, or whether there might exi
 st some unified approach that synthesizes the complementary advantages of 
 different techniques.\n\nIn this work\, we propose *relation transition sy
 stems* (or RTS's)\, a novel semantic model that marries together some of t
 he most appealing aspects of normal form bisimulations\, environmental bis
 imulations\, and Kripke logical relations. In particular\, RTS's combine t
 he elegant treatment of higher-order functions in normal form bisimulation
 s\, the coinductive (step-index-free) account of "cyclic" features in envi
 ronmental bisimulations\, and the use of transition systems for reasoning 
 about local state in Kripke logical relations. Furthermore\, RTS's enjoy t
 ransitivity of equivalence proofs\, and we have designed them to be scalab
 le to reasoning about equivalences between different languages. Thus\, we 
 have high hopes that RTS's will serve as an effective foundation for multi
 -language reasoning and\, in particular\, compositional multi-phase certif
 ied compilation.\n\nThis is joint work with Chung-Kil Hur\, Georg Neis\, a
 nd Viktor Vafeiadis\, to appear in POPL 2012.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR