Derek Dreyer, MPI-SWS; Microsoft Research Lectures

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

• Derek Dreyer, MPI-SWS
• Tuesday 18 May 2010, 14:00-15:00
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Abstract: Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages—-languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand 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 various 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 aspirations of the semantic cube to the powerful proof method of step-indexed Kripke logical relations. Building on recent work of Ahmed, Dreyer, and Rossberg, we define the first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call/cc. We then show how, under orthogonal restrictions to the expressive power of our language—-namely, the restriction to first-order state and/or the removal of call/cc—-we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate 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 properties of local state evolve over time. This is joint work with Georg Neis and Lars Birkedal.

Biography: Derek Dreyer received his PhD in Computer Science from Carnegie Mellon University in 2005. He then spent three years as a Research Assistant Professor at the Toyota Technological Institute at Chicago. Since January 2008, he has been an Independent Researcher at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany, where he heads the Type Systems and Functional Programming Group.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.