Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark (September 1981)
Kahn, G.: Natural Semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)
Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235–271 (1992)
Hoare, C.A.R., Hayes, I.J., Jifeng, H., Morgan, C.C., Roscoe, A.W., Sanders, J.W., Sorensen, I.H., Spivey, J.M., Sufrin, B.A.: Laws of programming. Commun. ACM 30, 672–686 (1987)
Isabelle/HOL proofs (2012), http://se.inf.ethz.ch/people/vanstaden/AlgebraUnifiesOperationalCalculi.thy
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)
Tony Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene Algebra. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 399–414. Springer, Heidelberg (2009)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Fokkink, W.: Introduction to Process Algebra, 1st edn. Springer-Verlag New York, Inc., New York (2000)
Roşu, G.: Programming Languages: A Rewriting Approach, http://fsl.cs.uiuc.edu/pub/pl.pdf
Plotkin, G.D.: The origins of structural operational semantics. Journal of Logic and Algebraic Programming 60-61, 3–15 (2004)
Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science 96(1), 217–248 (1992)
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)
Wehrman, I., Hoare, C.A.R., O’Hearn, P.W.: Graphical models of separation logic. Inf. Process. Lett. 109(17), 1001–1004 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Staden, S., Hoare, T. (2013). Algebra Unifies Operational Calculi. In: Wolff, B., Gaudel, MC., Feliachi, A. (eds) Unifying Theories of Programming. UTP 2012. Lecture Notes in Computer Science, vol 7681. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35705-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-35705-3_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35704-6
Online ISBN: 978-3-642-35705-3
eBook Packages: Computer ScienceComputer Science (R0)