Fourth Annual IEEE Symposium on

Logic in Computer Science (LICS 1989)

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

Authors: Howe, D.J.


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


    author = 	 {Howe, D.J.},
    title = 	 {Equality in lazy computation systems},
    booktitle =  {Proceedings of the Fourth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1989},
    year =	 1989,
    editor =	 {Rohit Parikh},
    month =	 {June}, 
    pages =      {198--203},
    location =   {Pacific Grove, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}