Advertisement

Algebra Unifies Operational Calculi

  • Stephan van Staden
  • Tony Hoare
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7681)

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.

Keywords

Inference Rule Operational Semantic Sequential Composition Operational Calculus Separation Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103(2), 235–271 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    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)zbMATHCrossRefGoogle Scholar
  5. 5.
  6. 6.
    Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)CrossRefGoogle Scholar
  9. 9.
    Fokkink, W.: Introduction to Process Algebra, 1st edn. Springer-Verlag New York, Inc., New York (2000)zbMATHGoogle Scholar
  10. 10.
    Roşu, G.: Programming Languages: A Rewriting Approach, http://fsl.cs.uiuc.edu/pub/pl.pdf
  11. 11.
    Plotkin, G.D.: The origins of structural operational semantics. Journal of Logic and Algebraic Programming 60-61, 3–15 (2004)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science 96(1), 217–248 (1992)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 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)
  14. 14.
    Wehrman, I., Hoare, C.A.R., O’Hearn, P.W.: Graphical models of separation logic. Inf. Process. Lett. 109(17), 1001–1004 (2009)MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Stephan van Staden
    • 1
  • Tony Hoare
    • 2
  1. 1.ETH ZurichSwitzerland
  2. 2.Microsoft ResearchCambridgeUnited Kingdom

Personalised recommendations