Logical Specification of Operational Semantics

  • Peter D. Mosses
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1683)


Various logic-based frameworks have been proposed for spe- cifying the operational semantics of programming languages and con- current systems, including inference systems in the styles advocated by Plotkin and by Kahn, Horn logic, equational specifications, reduction systems for evaluation contexts, rewriting logic, and tile logic. We consider the relationship between these frameworks, and assess their respective merits and drawbacks especially with regard to the modula- rity of specifications, which is a crucial feature for scaling up to practical applications.We also report on recent work towards the use of the Maude system (which provides an efficient implementation of rewriting logic) as a meta-tool for operational semantics.


Inference Rule Operational Semantic Reduction Rule Denotational Semantic Semantic Framework 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    E. Astesiano and G. Reggio. SMoLCS driven concurrent calculi. In TAPSOFT’87, Proc. Int. Joint Conf. on Theory and Practice of Software Development, Pisa, volume 249 of LNCS. Springer-Verlag, 1987.Google Scholar
  2. [2]
    D. Berry, R. Milner, and D. N. Turner. A semantics for ML concurrency primitives. In Proc. 17th Annual ACM Symposium on Principles of Programming Languages, pages 119–129. ACM, 1992.Google Scholar
  3. [3]
    R. Bruni, J. Meseguer, and U. Montanari. Process and term tile logic. Technical Report SRI-CSL-98-06, Computer Science Lab., SRI International, July 1998.Google Scholar
  4. [4]
    R. Cartwright and M. Felleisen. Extensible denotational language specifications. In M. Hagiya and J. C. Mitchell, editors, TACS’94, Symposium on Theoretical Aspects of Computer Software, volume 789 of LNCS, pages 244–272, Sendai, Japan, 1994. Springer-Verlag.CrossRefGoogle Scholar
  5. [5]
    M. Clavel, S. Eker, P. Lincoln, and J. Meseguer. Principles of Maude. In Meseguer [22], pages 65–89.Google Scholar
  6. [6]
    CoFI. The Common Framework Initiative for algebraic specification and development, electronic archives. Notes and Documents accessible by WWW1 and FTP2.Google Scholar
  7. [7]
    CoFI Language Design Task Group. CASL The CoFI Algebraic Specification Language Summary. Documents/CASL/Summary, in [6], Oct. 1998.Google Scholar
  8. [8]
    P. Cousot and R. Cousot. Inductive definitions, semantics, and abstract interpretation. In Proc. POPL’92, pages 83–94. ACM, 1992.Google Scholar
  9. [9]
    P. Degano and C. Priami. Enhanced operational semantics. ACM Computing Surveys, 28(2):352–354, June 1996.CrossRefGoogle Scholar
  10. [10]
    M. Felleisen and D. P. Friedman. Control operators, the SECD machine, and the _-calculus. In Formal Description of Programming Concepts III, Proc. IFIP TC2 Working Conference, Gl. Avern_s, 1986, pages 193–217. North-Holland, 1987.Google Scholar
  11. [11]
    M. Felleisen and R. Hieb. The reveised report on the syntactic theories of sequential control and state. Theoretical Comput. Sci., 102:235–271, 1992.CrossRefGoogle Scholar
  12. [12]
    W. Ferreira, M. Hennessy, and A. Jeffrey. A theory of weak bisumulation for core CML. J. Functional Programming, 8(5):447–451, 1998.MathSciNetCrossRefGoogle Scholar
  13. [13]
    F. Gadducci and U. Montanari. Tiles, rewriting rules, and CCS. In Meseguer [22].Google Scholar
  14. [14]
    F. Gadducci and U. Montanari. The tile model. In Proof, Language, and Interaction. The MIT Press, 1999. To appear.Google Scholar
  15. [15]
    R. Harper and C. Stone. A type-theoretic interpretation of Standard ML. In G. Plotkin, C. Stirling, and M. Tofte, editors, Robin Milner Festschrifft. MIT Press, 1998. To appear.Google Scholar
  16. [16]
    A. S. A. Jeffrey. Semantics for core concurrent ML using computation types. In A. D. Gordon and A. J. Pitts, editors, Higher Order Operational Techniques in Semantics, Proceedings. Cambridge University Press, 1997.Google Scholar
  17. [17]
    G. Kahn. Natural semantics. In STACS’87, Proc. Symp. on Theoretical Aspects of Computer Science, volume 247 of LNCS, pages 22–39. Springer-Verlag, 1987.Google Scholar
  18. [18]
    P. J. Landin. The mechanical evaluation of expressions. Computer Journal, 6:308–320, 1964.CrossRefGoogle Scholar
  19. [19]
    K. G. Larsen and L. Xinxin. Compositionality through operational semantics of contexts. In Proc. ICALP’90, volume 443 of LNCS, pages 526–539. Springer-Verlag, 1990.Google Scholar
  20. [20]
    N. Marti-Oliet and J. Meseguer. Rewriting logic as a logical and semantic framework. In D. Gabbay, editor, Handbook of Philosophical Logic, volume 6. Kluwer Academic Publishers, 1998. `Also Technical Report SRI-CSL-93-05, SRI International, August 1993.Google Scholar
  21. [21]
    J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 96(1):73–155, 1992.MathSciNetCrossRefGoogle Scholar
  22. [22]
    J. Meseguer, editor. First International Workshop on Rewriting Logic, volume 4 of Electronic Notes in Theoretical Computer Science, Asilomar (California), September 1996.Google Scholar
  23. [23]
    J. Meseguer. Rewriting logic as a semantic framework for concurrency: A progress report. In U. Montanari and V. Sassone, editors, Proc. CONCUR’96, volume 1119 of LNCS, pages 331–372. Springer-Verlag, 1996.Google Scholar
  24. [24]
    J. Meseguer. Membership algebra as a semantic framework for equational specification. In F. Parisi-Presicce, editor, Recent Trends in Algebraic Development Techniques, volume 1376 of LNCS, pages 18–61. Springer-Verlag, 1998.CrossRefGoogle Scholar
  25. [25]
    J. Meseguer and U. Montanari. Mapping tile logic into rewriting logic. In F. Parisi-Presicce, editor, Recent Trends in Algebraic Development Techniques, volume 1376 of LNCS. Springer-Verlag, 1998.Google Scholar
  26. [26]
    R. Milner. Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, A. Meyer, M. Nivat, M. Paterson, and D. Perrin, editors, Handbook of Theoretical Computer Science, volume B, chapter 19. Elsevier Science Publishers, Amsterdam; and MIT Press, 1990.Google Scholar
  27. [27]
    R. Milner and D. Sangiorgi. Barbed bisimulation. In Proc. ICALP’92, volume 623 of LNCS, pages 685–695. Springer-Verlag, 1992.Google Scholar
  28. [28]
    R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.Google Scholar
  29. [29]
    P. D. Mosses. Action Semantics. Number 26 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.Google Scholar
  30. [30]
    P. D. Mosses. Theory and practice of action semantics. In MFCS’ 96, Proc. 21st Int. Symp. on Mathematical Foundations of Computer Science (Cracow, Poland’ Sept. 1996), volume 1113 of LNCS, pages 37–61. Springer-Verlag, 1996.CrossRefGoogle Scholar
  31. [31]
    P. D. Mosses. Semantics, modularity, and rewriting logic. In C. Kirchner and H. Kirchner, editors, WRLA’98, Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, Pont-_a-Mousson, France, volume 15 of Electronic Notes in Theoretical Computer Science, 1998. Scholar
  32. [32]
    P. D. Mosses. Foundations of Modular SOS (extended abstract). In MFCS’99, Proc. 24th Intl. Symp. on Mathematical Foundations of Computer Science, Szklarska-Poreba, Poland, LNCS. Springer-Verlag, 1999. To appear.Google Scholar
  33. [33]
    P. D. Mosses. A modular SOS for Action Notation. Research series, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999. To appear. Draft available from{}pdm/.Google Scholar
  34. [34]
    P. D. Mosses. A modular SOS for Action Notation (extended abstract). Number NS-99-3 in Notes Series, BRICS, Dept. of Computer Science, Univ. of Aarhus, May 1999. Full version available [33].Google Scholar
  35. [35]
    A. M. Pitts and J. R. X. Ross. Process calculus based upon evaluation to committed form. In U. Montanari and V. Sassone, editors, Proc. CONCUR’96, volume 1119 of LNCS. Springer-Verlag, 1996.Google Scholar
  36. [36]
    G. D. Plotkin. Call-by-name, call-by-value, and the _-calculus. Theoretical Comput. Sci., 1:125–159, 1975.MathSciNetCrossRefGoogle Scholar
  37. [37]
    G. D. Plotkin. A structural approach to operational semantics. Lecture Notes DAIMI FN19, Dept. of Computer Science, Univ. of Aarhus, 1981.Google Scholar
  38. [38]
    C. Priami. Enhanced Operational Semantics for Concurrency. PhD thesis, Dipartimento di Informatica, Universit_a degli Studi di Pisa, 1996.Google Scholar
  39. [39]
    J. H. Reppy. CML: A higher-order concurrent language. In Proc. SIGPLAN’91, Conf. on Prog. Lang. Design and Impl., pages 293–305. ACM, 1991.Google Scholar
  40. [40]
    J. H. Reppy. Higher-Order Concurrency. PhD thesis, Computer Science Dept., Cornell Univ., 1992. Tech. Rep. TR 92-1285.Google Scholar
  41. [41]
    D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, Dept. of Computer Science, Univ. of Edinburgh,1992.Google Scholar
  42. [42]
    P. Sewell. From rewrite to bisimulation congruences. In Proc. CONCUR’98, volume 1466 of LNCS, pages 269–284. Springer-Verlag, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Peter D. Mosses
    • 1
  1. 1.BRICS and Department of Computer ScienceUniversity of AarhusNy Munkegade, bldg. 540Denmark

Personalised recommendations