Modular structural operational semantics. (English) Zbl 1072.68061

Summary: Modular SOS (MSOS) is a variant of conventional Structural Operational Semantics (SOS). Using MSOS, the transition rules for each construct of a programming language can be given incrementally, once and for all, and do not need reformulation when further constructs are added to the language. MSOS thus provides an exceptionally high degree of modularity in language descriptions, removing a shortcoming of the original SOS framework. After sketching the background and reviewing the main features of SOS, the paper explains the crucial differences between SOS and MSOS, and illustrates how MSOS descriptions are written. It also discusses standard notions of semantic equivalence based on MSOS. Appendix A shows how the illustrative MSOS rules given in the paper would be formulated in conventional SOS.


68Q55 Semantics in the theory of computing


Full Text: DOI Link


[1] Aceto, L; Fokkink, W; Verhoef, C, Structural operational semantics, (), 197-292, Chapter 3 · Zbl 1062.68074
[2] E. Astesiano. Inductive and operational semantics, in: E.J. Neuhold, M. Paul (Eds.), Formal Description of Programming Concepts, IFIP State-of-the-Art Report, Springer, 1991, pp. 51-136
[3] Astesiano, E; Bidoit, M; Krieg-Brückner, B; Mosses, P.D; Sannella, D; Tarlecki, A, C{\scasl}: the common algebraic specification language, Theoret. comput. sci., 286, 2, 153-196, (2002) · Zbl 1061.68103
[4] K.L. Bernstein, A congruence theorem for structured operational semantics of higher-order languages, in: Proc. LICS’98, IEEE, 1998, pp. 153-163
[5] D. Berry, R. Milner, D.N. Turner, A semantics for ML concurrency primitives, in: Proc. 17th Annual ACM Symposium on Principles of Programming Languages, ACM, 1992, pp. 119-129
[6] R. Cartwright, M. Felleisen, Extensible denotational language specifications, in: M. Hagiya, J.C. Mitchell (Eds.), TACS’94, Symposium on Theoretical Aspects of Computer Software, LNCS 789, Springer, 1994, pp. 244-272 · Zbl 0942.68544
[7] CoFI (The Common Framework Initiative). C{\scasl} Reference Manual. LNCS, 2960, IFIP Series. Springer, 2004
[8] Degano, P; Priami, C, Enhanced operational semantics, ACM comput. surv., 28, 2, 352-354, (1996)
[9] M. Felleisen, D.P. Friedman, Control operators, the SECD machine, and the λ-calculus, in: Formal Description of Programming Concepts III, Proc. IFIP TC2 Working Conference, 1986, North-Holland, 1987, pp. 193-217
[10] Fokkink, W.J; Verhoef, C, A conservative look at operational semantics with variable binding, Informat. comput., 146, 1, 24-54, (1998) · Zbl 0916.68098
[11] Gadducci, F; Montanari, U, The tile model, (), 133-166
[12] Hennessy, M, The semantics of programming languages: an elementary introduction using structural operational semanitcs, (1990), Wiley New York
[13] G. Kahn, Natural semantics, in: STACS’87, Proc. Symp. on Theoretical Aspects of Computer Science, LNCS 247, Springer, 1987, pp. 22-39 · Zbl 0635.68007
[14] S. Liang, P. Hudak, Modular denotational semantics for compiler construction. In: ESOP’96, Proc. 6th European Symposium on Programming, LNCS 1058, Springer, 1996, pp. 219-234
[15] Milner, R, Communication and concurrency, (1989), Prentice-Hall · Zbl 0683.68008
[16] R. Milner, Operational and algebraic semantics of concurrent processes, in: J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, vol. B, Elsevier Science Publishers, MIT Press, Amsterdam, 1990 (Chapter 19) · Zbl 0900.68217
[17] Milner, R; Tofte, M; Harper, R; MacQueen, D, The definition of standard ML (revised), (1997), The MIT Press
[18] E. Moggi, An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Computer Science Dept., University of Edinburgh, 1990
[19] P.D. Mosses, Action Semantics, Cambridge Tracts in Theoretical Computer Science 26. Cambridge University Press, 1992
[20] P.D. Mosses, Theory and practice of action semantics, in: MFCS’96 Proc. 21st Int. Symp. on Mathematical Foundations of Computer Science, Cracow, Poland, LNCS 1113, Springer, 1996, pp. 37-61
[21] P.D. Mosses, Semantics, modularity, and rewriting logic. in: WRLA’98, Proc. 2nd Int. Workshop on Rewriting Logic and its Applications, ENTCS 15, 1998
[22] P.D. Mosses, Foundations of modular SOS, Technical report, Dept. of Computer Science, Univ. of Aarhus, 1999. Full version of [23]
[23] 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 1672, Springer, 1999, pp. 70-80
[24] P.D. Mosses, Logical specification of operational semantics, in: CSL’99, Proc. Conf. on Computer Science Logic, LNCS 1683, Springer, 1999, pp. 32-49
[25] P.D. Mosses, A modular SOS for Action Notation. Technical report, Dept. of Computer Science, Univ. of Aarhus, 1999. Full version of [26]
[26] P.D. Mosses, A modular SOS for Action Notation (extended abstract), in: P.D. Mosses, D.A. Watt (Eds.), AS’99, Proc. 2nd International Workshop on Action Semantics, BRICS NS-99-3, Dept. of Computer Science, Univ. of Aarhus, 1999, pp. 131-142
[27] P.D. Mosses, A modular SOS for ML concurrency primitives, Technical report, Dept. of Computer Science, Univ. of Aarhus, 1999
[28] P.D. Mosses, AN-2: Revised action notation—syntax and semantics. Available at http://www.brics.dk/ pdm/papers/Mosses-AN-2-Semantics/, 2000
[29] P.D. Mosses, Pragmatics of modular SOS, in: A.M. Haeberer (Ed.), AMAST’02, Proc. 9th International Conference on Algebraic Methods and Software Technology, LNCS 2422, Springer, 2002, pp. 21-40 · Zbl 1275.68086
[30] Nielson, H.R; Nielson, F, Semantics with applications: A formal introduction, (1992), Wiley Chichester, UK · Zbl 0875.68626
[31] G.D. Plotkin, A structural approach to operational semantics. Technical report, Dept. of Computer Science, Univ. of Aarhus, 1981, Reprinted in JLAP, this issue, 2004
[32] G.D. Plotkin, J. Power, Adequacy for algebraic effects, in: F. Honsell, M. Miculan (Eds.), FOSSACS 2001, Foundations of Software Science and Computation Structures, LNCS 2030, Springer, 2001, pp. 1-24 · Zbl 0986.68055
[33] G.D. Plotkin, J. Power, Semantics for algebraic operations (extended abstract), in: S. Brookes, M. Mislove (Eds.), Proc. MFPS XVII, ENTCS 45. Elsevier, 2001 · Zbl 1260.68220
[34] G.D. Plotkin, J. Power, Notions of computation determine monads, in: M. Nielsen, U. Engberg (Eds.), FOSSACS 2002, Foundations of Software Science and Computation Structures, LNCS 2303, Springer, 2002, pp. 342-356 · Zbl 1077.68676
[35] J.H. Reppy, CML: A higher-order concurrent language, in: Proc. SIGPLAN’91, Conf. on Prog. Lang. Design and Impl., ACM, 1991, pp. 293-305
[36] J.H. Reppy, Higher-Order Concurrency, Ph.D. thesis, Computer Science Dept., Cornell Univ., 1992. Tech. Rep. TR 92-1285
[37] J.C. Reynolds, Using category theory to define implicit coercions and generic operators, in: N.D. Jones (Ed.), Semantics-Directed Compiler Generation, LNCS 94, Springer, 1980, pp. 211-258
[38] Slonneger, K; Kurtz, B.L, Formal syntax and semantics of programming languages: A laboratory based approach, (1995), Addison-Wesley · Zbl 0844.68016
[39] D. Turi, G.D. Plotkin, Towards a mathematical operational semantics, in: Proc. LICS’97, IEEE, 1997
[40] K. Wansbrough, A modular monadic action semantics, Master’s thesis, Dept. of Computer Science, Univ. of Auckland, 1997
[41] K. Wansbrough, J. Hamer, A modular monadic action semantics, in: Conference on Domain-Specific Languages, The USENIX Association, 1997, pp. 157-170
[42] Winskel, G, The formal semantics of programming languages: an introduction, (1993), MIT Press · Zbl 0919.68082
[43] A. Wright, M. Felleisen, A syntactic approach to type soundness, Technical Report TR91-160, Dept. of Computer Science, Rice University, 1991 · Zbl 0938.68559
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.