Relational interpretations of type systems are useful for establishing
properties of programming languages. For languages with recursive types it is
difficult to establish the existence of a relational interpretation. The usual
approach is to pass to a domain-theoretic model of the language, and
exploiting the structure of the model to derive relations properties of it. We
investigate the construction of relational interpretations of recursive types
in a purely operational setting, drawing on recent ideas from domain theory
and operational semantics as a guide. We prove syntactic minimal invariance
for an extension of PCF with a recursive type, a syntactic analogue of the
minimal invariance property used by Freyd and Pitts to characterize the domain
interpretation of a recursive type. As Pitts has shown in the setting of
domains, syntactic minimal invariance suffices to establish the existence of
relational interpretations. We give two applications of this
construction. First, we derive a notion of logical equivalence for expressions
of the language that we show coincides with experimental equivalence and
which, by virtue of its construction, validates useful induction and
coinduction principles for reasoning about the recursive type. Second, we give
a relational proof of correctness of the continuation-passing transformation,
which is used in some compilers for functional languages.