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

Authors: Ian A. Mason Carolyn L. Talcott

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 = 	 {Ian A. Mason and Carolyn L. Talcott},
    title = 	 {References, local variables and operational reasoning},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {186--197},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }