@INPROCEEDINGS{PittsAM:compavm,
AUTHOR={A.~M.~Pitts},
TITLE={Computational Adequacy via `Mixed' Inductive Definitions},
BOOKTITLE={Mathematical Foundations of Programming Semantics, Proc.\
9th Int.\ Conf., {New} {Orleans}, LA, USA, April 1993},
SERIES={Lecture Notes in Computer Science},
VOLUME=802,
PUBLISHER={Springer-Verlag, Berlin},
YEAR=1994,
PAGES={72--82},
ABSTRACT={For programming languages whose denotational semantics uses
fixed points of domain constructors of mixed variance, proofs of
correspondence between operational and denotational semantics
(or between two different denotational semantics) often depend upon
the existence of relations specified as the fixed point of
non-monotonic operators. This paper describes a new approach to
constructing such relations which avoids having to delve into
the detailed construction of the recursively defined domains
themselves. The method is introduced by example, by considering
the proof of computational adequacy of a denotational semantics
for expression evaluation in a simple, untyped functional
programming language.}}