CMU-CS-98-125Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-98-125
Lars Birkedal, Robert Harper April 1998
[Submitted for publication to
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.
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |