University of Cambridge > > Microsoft Research Cambridge, public talks > The Marriage of Bisimulations and Kripke Logical Relations

The Marriage of Bisimulations and Kripke Logical Relations

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

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 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2019, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity