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 contextual equivalence of programs involving
this combination of functional and procedural features. The method is
based upon the use of a certain kind of 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 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 `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.