References, local variables and operational reasoning
- 2 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 186-197
- https://doi.org/10.1109/lics.1992.185532
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.Keywords
This publication has 19 references indexed in Scilit:
- Semantical Analysis of Specification Logic, 2Published by Springer Nature ,1997
- Inferring the equivalence of functional programs that mutate dataTheoretical Computer Science, 1992
- Equivalence in functional languages with effectsJournal of Functional Programming, 1991
- Type inference for polymorphic referencesInformation and Computation, 1990
- Problematic features of programming languages: a situational-calculus approachActa Informatica, 1981
- Call-by-name, call-by-value and the λ-calculusTheoretical Computer Science, 1975
- A language and axioms for explicit mathematicsPublished by Springer Nature ,1975
- The next 700 programming languagesCommunications of the ACM, 1966
- Correspondence between ALGOL 60 and Church's Lambda-notationCommunications of the ACM, 1965
- The Mechanical Evaluation of ExpressionsThe Computer Journal, 1964