Relational Interpretations of Recursive Types in an Operational Setting

AbstractRelational 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 relational 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