Abstract
A novel form of labelled transition system is proposed, where the labels are the arrows of a category, and adjacent labels in computations are required to be composable. Such transition systems provide the foundations for modular SOS descriptions of programming languages. Three fundamental ways of transforming label categories, analogous to monad transformers, are provided, and it is shown that their applications preserve computations in modular SOS. The approach is illustrated with fragments taken from a modular SOS for ML concurrency primitives.
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
E. Astesiano. Inductive and operational semantics. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts, IFIP State-of-the-Art Report, pages 51–136. Springer-Verlag, 1991.
K. L. Bernstein. A congruence theorem for structured operational semantics of higher-order languages. In Proc. LICS’98, pages 153–163. IEEE, 1998.
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.
R. Cartwright and M. Felleisen. Extensible denotational language specifications. In M. Hagiya and J. C. Mitchell, editors, Symposium on Theoretical Aspects of Computer Software, number 789 in LNCS, pages 244–272, Sendai, Japan, Apr. 1994. Springer-Verlag.
P. Degano and C. Priami. Enhanced operational semantics. A CM Computing Surveys, 28(2):352–354, June 1996.
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. Avenues, 1986, pages 193–217. North-Holland, 1987.
W. Fokkink and R. van Glabbeek. Ntyft/ntyxt rules reduce to ntree rules. Information and Computation, 126(1):1–10, 1996.
W. J. Fokkink and C. Verhoef. A conservative look at operational semantics with variable binding. Information and Computation, 146(1):24–54, 1998.
F. Gadducci and U. Montanari. The tile model. In Proof, Language, and Interaction. The MIT Press, 1999. To appear.
M. Hennessy. The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley, New York, 1990.
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.
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.
R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.
P. D. Mosses. Action semantics. Home page: http://www.brics.dk/Projects/AS/.
P. D. Mosses. Action Semantics. Number 26 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.
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.
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-à-Mousson, France, volume 15 of Electronic Notes in Theoretical Computer Science, 1998. http://www.elsevier.nl/locate/entcs/volume15.html.
P. D. Mosses. Foundations of modular SOS. BRICS Report Series, BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999.
P. D. Mosses. A modular SOS for action notation (extended abstract). In P. D. Mosses, editor, Proc. 2nd Int. Workshop on Action Semantics, Amsterdam, 1999, BRICS Notes Series. BRICS, Dept. of Computer Science, Univ. of Aarhus, 1999.
P. D. Mosses. A modular SOS for ML concurrency primitives. Draft, available from http://www.brics.dk/pdm/, Apr. 1999.
H. R. Nielson and F. Nielson. Semantics with Applications: A Formal Introduction. Wiley, Chichester, UK, 1992.
G. D. Plotkin. A structural approach to operational semantics. Lecture Notes DAIMI FN-19, Dept. of Computer Science, Univ. of Aarhus, 1981.
G. D. Plotkin. An operational semantics for CSP. In D. Bjørner, editor, Formal Description of Programming Concepts II, Proc. IFIP TC2 Working Conference, Garmisch-Partenkirchen, 1982. IFIP, North-Holland, 1983.
C. Priami. Enhanced Operational Semantics for Concurrency. PhD thesis, Dipartimento di Informatica, Università degli Studi di Pisa, 1996.
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.
J. H. Reppy. Higher-Order Concurrency. PhD thesis, Computer Science Dept., Cornell Univ., 1992. Tech. Rep. TR 92-1285.
K. Slonneger and B. L. Kurtz. Formal Syntax and Semantics of Programming Languages: A Laboratory Based Approach. Addison-Wesley, 1995.
D. Turi and G. D. Plotkin. Towards a mathematical operational semantics. In Proc. LICS’97, pages 280–291. IEEE, 1997.
A. Wright and M. Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Dept. of Computer Science, Rice University, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mosses, P.D. (1999). Foundations of Modular SOS. In: Kutyłowski, M., Pacholski, L., Wierzbicki, T. (eds) Mathematical Foundations of Computer Science 1999. MFCS 1999. Lecture Notes in Computer Science, vol 1672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48340-3_7
Download citation
DOI: https://doi.org/10.1007/3-540-48340-3_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66408-6
Online ISBN: 978-3-540-48340-3
eBook Packages: Springer Book Archive