@INCOLLECTION{PittsAM:operfl,
AUTHOR={A.~M.~Pitts and I.~D.~B.~Stark},
TITLE={Operational Reasoning for Functions with Local State},
BOOKTITLE={Higher Order Operational Techniques in Semantics},
EDITOR={A.~D.~Gordon and A.~M.~Pitts},
YEAR=1998,
PUBLISHER={Cambridge University Press},
SERIES={Publications of the Newton Institute},
PAGES={227--273},
ABSRACT={Languages such as ML or Lisp permit the use of recursively defined
function expressions with locally declared storage locations.
Although this can be very convenient from a programming point of
view it severely complicates the properties of program equivalence
even for relatively simple fragments of such languages---such as the
simply typed fragment of Standard~ML with integer-valued references
considered here. This paper presents a method for reasoning about
\emph{contextual equivalence} of programs involving this combination
of functional and procedural features. The method is based upon the
use of a certain kind of \emph{logical relation} parameterised by
relations between program states. The form of this logical relation
is novel, in as much as it involves relations not only between
program expressions, but also between program continuations (also
known as \emph{evaluation contexts}). The authors found this
approach necessary in order to establish the `Fundamental Property
of logical relations' in the presence of both dynamically allocated
local state and recursion. The logical relation characterises
contextual equivalence and yields a proof of the best known context
lemma for this kind of language---the Mason-Talcott \Quote{ciu}
theorem. Moreover, it is shown that the method can prove examples
where such a context lemma is not much help and which involve
representation independence, higher order memoising functions, and
profiling functions.}
}