Algebra, Logic, Locality, Concurrency

  • Peter W. O’Hearn
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)


This talk reports on ongoing work - with Tony Hoare, Akbar Hussain, Bernhard Möller, Rasmus Petersen, Georg Struth, Ian Wehrman, and others - on models and logics for concurrent processes [10,6,5]. The approach we are taking abstracts from syntax or particular models. Message passing and shared memory process interaction, and strong (interleaving) and weak (partial order) approaches to sequencing, are accomodated as different models of the same core axioms. Rules of program logic, related to Hoare and Separation logics, flow at once from the algebraic axioms. So, one gets a generic program logic from the algebra, which holds for a range of concrete models.


  1. 1.
    Bloom, S.L., Ésik, Z.: Free shuffle algebras in language varieties. Theor. Comput. Sci. 163(1&2), 55–98 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Brookes, S.D.: A semantics of concurrent separation logic. Theoretical Computer Science 375(1-3), 227–270 (2007); Prelim. version appeared in CONCUR 2004MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS, pp. 366–378. IEEE Computer Society (2007)Google Scholar
  4. 4.
    Gischer, J.L.: The equational theory of pomsets. Theor. Comput. Sci. 61, 199–224 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Hoare, C.A.R., Hussain, A., Möller, B., O’Hearn, P.W., Petersen, R.L., Struth, G.: On Locality and the Exchange Law for Concurrent Processes. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011 – Concurrency Theory. LNCS, vol. 6901, pp. 250–264. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Hoare, T., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program (2011); Preliminary verson in CONCUR 2009Google Scholar
  7. 7.
    O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007); Prelim. version appeared in CONCUR 2004MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–9. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    Pratt, V.: Modelling concurrency with partial orders. International Journal of Parallel Programming 15(1), 33–71 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Wehrman, I., Hoare, C.A.R., O’Hearn, P.W.: Graphical models of separation logic. Inf. Process. Lett. 109(17), 1001–1004 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Winskel, G.: Events in Computation. Ph.D. thesis, University of Edinburgh (1980)Google Scholar
  12. 12.
    Yang, H., O’Hearn, P.W.: A Semantic Basis for Local Reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Peter W. O’Hearn
    • 1
  1. 1.Queen Mary University of LondonUK

Personalised recommendations