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