BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Derek Dreyer\, MPI-SWS\; Microsoft Research Lectures - Derek Dreye
 r\, MPI-SWS
DTSTART:20100518T130000Z
DTEND:20100518T140000Z
UID:TALK24894@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:*Abstract:* Reasoning about program equivalence is one of the 
 oldest problems in semantics. In recent years\, useful techniques have bee
 n developed\, based on bisimulations and logical relations\, for reasoning
  about equivalence in the setting of increasingly realistic languages---la
 nguages nearly as complex as ML or Haskell. Much of the recent work in thi
 s direction has considered the interesting representation independence pri
 nciples enabled by the use of local state\, but it is also important to un
 derstand the principles that powerful features like higher-order state and
  control effects disable. This latter topic has been broached extensively 
 within the framework of game semantics\, resulting in what Abramsky dubbed
  the `semantic cube`: fully abstract game-semantic characterizations of va
 rious axes in the design space of ML-like languages. But when it comes to 
 reasoning about many actual examples\, game semantics does not yet supply 
 a useful technique for proving equivalences. In this work\, we marry the a
 spirations of the semantic cube to the powerful proof method of step-index
 ed Kripke logical relations. Building on recent work of Ahmed\, Dreyer\, a
 nd Rossberg\, we define the first fully abstract logical relation for an M
 L-like language with recursive types\, abstract types\, general references
  and call/cc. We then show how\, under orthogonal restrictions to the expr
 essive power of our language---namely\, the restriction to first-order sta
 te and/or the removal of call/cc---we can enhance the proving power of our
  possible-worlds model in correspondingly orthogonal ways\, and we demonst
 rate this proving power on a range of interesting examples. Central to our
  story is the use of state transition systems to model the way in which pr
 operties of local state evolve over time. This is joint work with Georg Ne
 is and Lars Birkedal. \n\n*Biography:* Derek Dreyer received his PhD in Co
 mputer Science from Carnegie Mellon University in 2005.  He then spent thr
 ee years as a Research Assistant Professor at the Toyota Technological Ins
 titute at Chicago.  Since January 2008\, he has been an Independent Resear
 cher at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbru
 ecken\, Germany\, where he heads the Type Systems and Functional Programmi
 ng Group.
LOCATION:Small public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR