Algebra Unifies Operational Calculi
We survey the well-known algebraic laws of sequential programming, and propose some less familiar laws for concurrent programming. On the basis of these laws, we derive a general calculus of program execution. The basic judgment of the theory is a quintuple, and we deduce its rules by algebraic reasoning. The general calculus can be specialised to obtain more familiar operational calculi, such as the structural operational semantics of Plotkin, process calculus semantics of Milner, reduction semantics with evaluation contexts of Felleisen and Hieb, and the natural semantics of Kahn. The algebra unifies these calculi, as it is simpler than each calculus derived from it, and stronger than all of them put together.
KeywordsInference Rule Operational Semantic Sequential Composition Operational Calculus Separation Logic
Unable to display preview. Download preview PDF.
- 1.Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark (September 1981)Google Scholar
- 5.Isabelle/HOL proofs (2012), http://se.inf.ethz.ch/people/vanstaden/AlgebraUnifiesOperationalCalculi.thy
- 10.Roşu, G.: Programming Languages: A Rewriting Approach, http://fsl.cs.uiuc.edu/pub/pl.pdf
- 13.Nielson, H.R., Nielson, F.: Semantics with Applications: A Formal Introduction, Revised edn. (July 1999), http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html; Original edition published by John Wiley & Sons (1992)