zbMATH — the first resource for mathematics

Operational reasoning for functions with local state. (English) Zbl 0967.68035
Gordon, Andrew D. (ed.) et al., Higher order operational techniques in semantics. Papers from the HOOTS workshop, Cambridge, UK, October 1995. Cambridge: Cambridge University Press. Publ. Newton Inst. 12, 227-273 (1998).
Summary: 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 parameterized 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 characterizes 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 memoizing functions, and profiling functions.
For the entire collection see [Zbl 0942.00062].

68N18 Functional programming and lambda calculus