References, local variables and operational reasoning

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