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