Logic in Computer Science (LICS 1992)

Paper: References, local variables and operational reasoning (at LICS 1992)

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

Abstract

A.R. Meyer and K. Sieber (Proc. 15th ACM. Symp. on Principles of Programming Languages, 1988, p.191-208) gave a series of examples of programs that are operationally equivalent (according to the intended semantics of block-structured Algol-like programs) but are not given equivalent denotations in traditional denotational semantics. They propose various modifications to the denotational semantics that solve some of these discrepancies, but not all. The present authors approach the same problem, but from an operational rather than a denotational perspective. They present the first-order part of a new logic for reasoning about programs, and they use this logic to prove the equivalence of the Meyer-Sieber examples

BibTeX

  @InProceedings{MasonTalcott-Referenceslocalvari,
    author = 	 {Mason, I.A. and Talcott, C.L.},
    title = 	 {References, local variables and operational reasoning},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {186--197},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }