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 isto pass to a domaintheoretic 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.