Relational interpretations of recursive types in an operational setting

Abstract

Relational interpretations of type systems are a useful tool for establishing properties of programming languages. For languages with recursive types the existence of a relational interpretation is often difficult to establish. The most well-known approach is to pass to a domain theoretic model of the language, using the structure of the domain to define a suitable system of relations. Here we study the construction of relational interpretations for an ML-like language with recursive functions and recursive types in a purely operational setting. The construction is an adaptation of results of Pitts on relational properties of domains to an operational setting, making use of techniques introduced by Mason, Smith, and Talcott for proving operational equivalence of expressions. To illustrate the method we give a relational proof of correctness of the continuation-passing transformation used in some compilers for functional languages.