CMU-CS-98-125
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-98-125

Relational Interpretations of Recursive Types in an Operational Setting

Lars Birkedal, Robert Harper

April 1998

[Submitted for publication to Information and Computation.
A summary of this paper appeared in TACS '97.]

CMU-CS-98-125.ps


Relational interpretations of type systems are useful for establishing properties of programming languages. For languages with recursive types it is usually difficult to establish the existence of a relational interpretation. The usual approach is to give a denotational semantics of the language in a domain-theoretic model given by an inverse limit construction, and to construct relations over the model by a similar inverse limit construction. However, in passing to a denotational semantics we incur the obligation to prove its adequacy with respect to the operational semantics of the language, which is itself often proved using a relational interpretation of types! In this paper 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 establish a syntactic minimal invariance property for an ML-like language with a recursive type that is a syntactic analogue of Freyd's universal characterization of the canonical solution of a domain equation. As Pitts has shown in the setting of domans, minimal invariance suffices to establish the existence of relational interpretations of recursive types. 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 contextual 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. The proof relies on the construction of a family of simulation relations whose existence follows from syntactic minimal invariance.

Keywords: Type theory, operational semantics, logical relations, equational logics, compiler correctness, continuations


76 pages


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu