Report Number: CS-TR-89-1250
Institution: Stanford University, Department of Computer Science
Title: A sound and complete axiomatization of operational equivalence between programs with memory
Author: Mason, Ian
Author: Talcott, Carolyn
Date: March 1989
Abstract: In this paper we present a formal system for deriving assertions about programs with memory. The assertions we consider are of the following three forms: (i) e diverges (i.e. fails to reduce to a value), written $\arru e$; (ii) $e_O$ and $e_1$ reduce to the same value and have exactly the same effect on memory, written $e_O \bksimlr e_1$; and (iii) $e_O$ and $e_1$ reduce to the same value and have the same effect on memory up to production of garbage (are strongly isomorphic), written $_O \bksimeq e_1$. The e, $e_j$ are expressions of a first-order Scheme- or Lisp-like language with the data operations atom, eq, car, cdr, cons, setcar, setcdr, the control primitives let and if, and recursive definition of function symbols.
http://i.stanford.edu/pub/cstr/reports/cs/tr/89/1250/CS-TR-89-1250.pdf