Paper: Equality in lazy computation systems (at LICS 1989)

Authors: Douglas J. Howe

Abstract

The author introduces a general class of lazy computation systems and defines a natural program equivalence for them. He proves that if an extensionality condition holds of each of the operators of a computational system, then the equivalence relation is a congruence, so that the usual kinds of equality reasoning are valid for it. This condition is a simple syntactic one and is easy to verify for the various lazy computation systems considered so far. Conditions are given under which the equivalence coincides with observational congruence. These results have important consequences for type theories

BibTeX

  @InProceedings{Howe-Equalityinlazycompu,
    author = 	 {Douglas J. Howe},
    title = 	 {Equality in lazy computation systems},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)},
    year =	 {1989},
    month =	 {June}, 
    pages =      {198--203},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }