Ian Stark

Operational Reasoning for Functions with Local State

Andrew Pitts and Ian Stark

In Gordon and Pitts, editors, Higher Order Operational Techniques in Semantics, pages 227-273. Publications of the Newton Institute, Cambridge University Press, 1998.

Fetch paper (PDF, 244k). Go to publications, talks or home page.


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.

  author =       {Andrew Pitts and Ian Stark},
  title =        {Operational Reasoning for Functions with Local
  booktitle =    {Higher Order Operational Techniques in Semantics},
  editor =       {Andrew Gordon and Andrew Pitts},
  year =         {1998},
  pages =        {227--273},
  publisher =    {Publications of the Newton Institute, Cambridge
                  University Press}, 
  url =          {http://www.inf.ed.ac.uk/~stark/operfl.html},

Page last modified: Tuesday 5 August 2008