Abstract

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 .