Article

Operational Semantics and Program Equivalence

Author:

Andrew M. PittsAuthors Info & Claims

Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures

Pages 378 - 412

Published: 09 September 2000 Publication History

Abstract

This tutorial paper discusses a particular style of operational semantics that enables one to give a 'syntax-directed' inductive definition of termination which is very useful for reasoning about operational equivalence of programs. We restrict attention to contextual equivalence of expressions in the ML family of programming languages, concentrating on functions involving local state. A brief tour of structural operational semantics culminates in a structural definition of termination via an abstract machine using 'frame stacks'. Applications of this to reasoning about contextual equivalence are given.

References

[1]

K. Aboul-Hosn and J. Hannan. Program equivalence with private state. Preprint., January 2002.

[2]

P. N. Benton and A. J. Kennedy. Monads, effects and transformations. In A. D. Gordon and A. M. Pitts, editors, HOOTS '99 Higher Order Operational Techniques in Semantics, Paris, France, September 1999 , volume 26 of Electronic Notes in Theoretical Computer Science . Elsevier, 1999.

[3]

G. M. Bierman, A. M. Pitts, and C. V. Russo. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Fourth International Workshop on Higher Order Operational Techniques in Semantics, Montréal , volume 41 of Electronic Notes in Theoretical Computer Science . Elsevier, September 2000.

[4]

L. Birkedal and R. Harper. Relational interpretation of recursive types in an operational setting (Summary). In M. Abadi and T. Ito, editors, Theoretical Aspects of Computer Software, Third International Symposium, TACS'97, Sendai, Japan, September 23 - 26, 1997, Proceedings , volume 1281 of Lecture Notes in Computer Science . Springer-Verlag, Berlin, 1997.

[5]

G. Cousineau and M. Mauny. The Functional Approach to Programming . Cambridge University Press, 1998.

[6]

R. Harper and C. Stone. An interpretation of Standard ML in type theory. Technical Report CMU-CS-97-147, Carnegie Mellon University, Pittsburgh, PA, 1997.

[7]

A. Jeffrey and J. Rathke. Towards a theory of bisimulation for local names. In 14th Annual Symposium on Logic in Computer Science , pages 56-66. IEEE Computer Society Press, Washington, 1999.

[8]

G. Kahn. Natural semantics. Rapport de Recherche 601, INRIA, Sophia-Antipolis, France, 1987.

[9]

R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised) . MIT Press, 1997.

[10]

P. W. O'Hearn and J. G. Riecke. Kripke logical relations and PCF. Information and Computation , 120:107-116, 1995.

[11]

A. M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation , Publications of the Newton Institute, pages 241-298. Cambridge University Press, 1997.

[12]

A. M. Pitts. Reasoning about local variables with operationally-based logical relations. In P. W. O'Hearn and R. D. Tennent, editors, Algol-Like Languages , volume 2, chapter 17, pages 173-193. Birkhauser, 1997. First appeared in Proceedings 11th Annual IEEE Symposium on Logic in Computer Science , Brunswick, NJ, July 1996, pp 152-163.

[13]

A. M. Pitts. Existential types: Logical relations and operational equivalence. In K. G. Larsen, S. Skyum, and G. Winskel, editors, Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, Denmark, July 1998, Proceedings , volume 1443 of Lecture Notes in Computer Science , pages 309- 326. Springer-Verlag, Berlin, 1998.

[14]

A. M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science , 10:321-359, 2000.

[15]

A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In A. D. Gordon and A. M. Pitts, editors, Higher Order Operational Techniques in Semantics , Publications of the Newton Institute, pages 227-273. Cambridge University Press, 1998.

[16]

G. D. Plotkin. Lambda-definability and logical relations. Memorandum SAI-RM- 4, School of Artificial Intelligence, University of Edinburgh, 1973.

[17]

G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981.

[18]

A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation , 115:38-94, 1994.

Cited By

Hackett JHutton G(2019)Call-by-need is clairvoyant call-by-valueProceedings of the ACM on Programming Languages10.1145/33417183:ICFP(1-23)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341718
Nishida YIgarashi ASabel DThiemann P(2018)Nondeterministic Manifest ContractsProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236964(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236964
Schäfer SSchneider SSmolka GAvigad JChlipala A(2016)Axiomatic semantics for compiler verificationProceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs10.1145/2854065.2854083(188-196)Online publication date: 18-Jan-2016
https://dl.acm.org/doi/10.1145/2854065.2854083
Show More Cited By

Operational Semantics and Program Equivalence
1. Theory of computation
  1. Semantics and reasoning

Recommendations

Equivalence of formal semantics definition methods
Abstract
There are numerous methods of formally defining the semantics of computer languages. Each method has been designed to fulfil a different purpose. For example, some have been designed to make reasoning about languages as easy as possible; others ...
Coinductive big-step operational semantics

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We ...
Operational semantics of programming languages
Proceedings of ACM conference on Proving assertions about programs

A framework is developed for the operational characterization of the semantics of computational formalisms such as programming languages, digital computers and automata. Operational semantics is contrasted with input-output semantics and it is shown ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures

September 2000

536 pages

ISBN:3540440445

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 09 September 2000

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Hackett JHutton G(2019)Call-by-need is clairvoyant call-by-valueProceedings of the ACM on Programming Languages10.1145/33417183:ICFP(1-23)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341718
Nishida YIgarashi ASabel DThiemann P(2018)Nondeterministic Manifest ContractsProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236964(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236964
Schäfer SSchneider SSmolka GAvigad JChlipala A(2016)Axiomatic semantics for compiler verificationProceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs10.1145/2854065.2854083(188-196)Online publication date: 18-Jan-2016
https://dl.acm.org/doi/10.1145/2854065.2854083
Gammie PHosking AEngelhardt K(2015)Relaxing safely: verified on-the-fly garbage collection for x86-TSOACM SIGPLAN Notices10.1145/2813885.273800650:6(99-109)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2813885.2738006
Gammie PHosking AEngelhardt KGrove DBlackburn S(2015)Relaxing safely: verified on-the-fly garbage collection for x86-TSOProceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2737924.2738006(99-109)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1145/2737924.2738006
Lösch SPitts A(2014)Denotational Semantics with Nominal Scott DomainsJournal of the ACM10.1145/262952961:4(1-46)Online publication date: 1-Jul-2014
https://dl.acm.org/doi/10.1145/2629529
Lakin MPitts A(2012)Encoding Abstract Syntax Without Fresh NamesJournal of Automated Reasoning10.1007/s10817-011-9220-749:2(115-140)Online publication date: 1-Aug-2012
https://dl.acm.org/doi/10.1007/s10817-011-9220-7
Ahmed AAppel ARichards CSwadi KTan GWang D(2010)Semantic foundations for typed assembly languagesACM Transactions on Programming Languages and Systems10.1145/1709093.170909432:3(1-67)Online publication date: 16-Mar-2010
https://dl.acm.org/doi/10.1145/1709093.1709094
Schmidt-Schauß MSabel D(2010)Closures of may-, should- and must-convergences for contextual equivalenceInformation Processing Letters10.1016/j.ipl.2010.01.001110:6(232-235)Online publication date: 1-Feb-2010
https://dl.acm.org/doi/10.1016/j.ipl.2010.01.001
Ridge T(2009)Verifying distributed systemsACM SIGPLAN Notices10.1145/1594834.148093444:1(429-440)Online publication date: 21-Jan-2009
https://dl.acm.org/doi/10.1145/1594834.1480934
Show More Cited By

View Options

View options

Figures

Tables

Media

View Table of Conten