The Marriage of Bisimulations and Kripke Logical Relations

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

• Derek Dreyer, MPI-SWS
• Tuesday 01 November 2011, 15:00-16:00
• Small lecture theatre, 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.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

There has been great progress in recent years on developing practical techniques for reasoning about program equivalence in ML-like languages—-that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. What has not emerged thus far is a clear understanding of how the different families of techniques relate to one another, or whether there might exist some unified approach that synthesizes the complementary advantages of different techniques.

In this work, we propose relation transition systems (or RTS ’s), a novel semantic model that marries together some of the most appealing aspects of normal form bisimulations, environmental bisimulations, and Kripke logical relations. In particular, RTS ’s combine the elegant treatment of higher-order functions in normal form bisimulations, the coinductive (step-index-free) account of “cyclic” features in environmental bisimulations, and the use of transition systems for reasoning about local state in Kripke logical relations. Furthermore, RTS ’s enjoy transitivity of equivalence proofs, and we have designed them to be scalable 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 certified compilation.

This is joint work with Chung-Kil Hur, Georg Neis, and Viktor Vafeiadis, to appear in POPL 2012 .

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 lecture theatre, 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.