## 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.

### Abstract

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.

@InCollection{pitts/stark:operfl,
author = {Andrew Pitts and Ian Stark},
title = {Operational Reasoning for Functions with Local
State},
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