Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

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: 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) 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

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}
  }
   

Last modified: 2017-04-0512:37
Andrzej Murawski