@INCOLLECTION{PittsAM:realvo,
AUTHOR={A.~M.~Pitts},
TITLE={Reasoning About Local Variables with Operationally-Based
Logical Relations},
BOOKTITLE={Algol-Like Languages},
EDITOR={P.~W.~O'Hearn and R.~D.~Tennent},
VOLUME=2,
CHAPTER=17,
PUBLISHER={Birkhauser},
YEAR=1997,
PAGES={173--193},
NOTE={Reprinted from \emph{Proceedings Eleventh Annual IEEE
Symposium on Logic in Computer Science}, Brunswick, NJ, July 1996,
pp~152--163.},
ABSTRACT={A parametric logical relation between the phrases of an Algol-like
language is presented. Its definition involves the structural
operational semantics of the language, but was inspired by recent
denotationally-based work of O'Hearn and Reynolds on translating Algol
into a predicatively polymorphic linear lambda calculus. The logical
relation yields an applicative characterisation of contextual
equivalence for the language and provides a useful (and complete)
method for proving equivalences. Its utility is illustrated by giving
simple and direct proofs of some contextual equivalences, including an
interesting equivalence due to O'Hearn which hinges upon the
undefinability of `snapback' operations (and which goes beyond the
standard suite of `Meyer-Sieber' examples). Whilst some of the
mathematical intricacies of denotational semantics are avoided, the
hard work in this operational approach lies in establishing the
`fundamental property' for the logical relation---the proof of which
makes use of a compactness property of fixpoint recursion with respect
to evaluation of phrases. But once this property has been established,
the logical relation provides a verification method with an
attractively low mathematical overhead.}
}