Fourth Annual IEEE Symposium on

Logic in Computer Science (LICS 1989)

Paper: Axiomatizing operational equivalence in the presence of side effects (at LICS 1989)

Authors: Mason, I.A. Talcott, C.


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) e0 and e1 are strongly isomorphic (i.e. reduce to the same value and have the same effect on memory up to production of garbage). The e, ej 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


    author = 	 {Mason, I.A. and Talcott, C.},
    title = 	 {Axiomatizing operational equivalence in the presence of side effects },
    booktitle =  {Proceedings of the Fourth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1989},
    year =	 1989,
    editor =	 {Rohit Parikh},
    month =	 {June}, 
    pages =      {284--293},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}