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

Authors: Ian A. Mason Carolyn L. Talcott

Abstract

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

BibTeX

  @InProceedings{MasonTalcott-Axiomatizingoperati,
    author = 	 {Ian A. Mason and Carolyn L. Talcott},
    title = 	 {Axiomatizing operational equivalence in the presence of side effects },
    booktitle =  {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)},
    year =	 {1989},
    month =	 {June}, 
    pages =      {284--293},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }