Axiomatizing operational equivalence in the presence of side effects

The authors present a formal system for deriving assertions about programs with side effects. The assertions considered are the following: (i) the expression e diverges (i.e. fails to reduce to a value); and (ii) e₀ and e₁ are strongly isomorphic (i.e. reduce to the same value and have the same effect on memory up to production of garbage). 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