Abstract
In the mid-nineties, Turi and Plotkin gave an elegant categorical treatment of denotational and operational semantics for process algebra-like languages, proving compositionality and adequacy by defining operational semantics as a distributive law of syntax over behaviour. However, its applications to stateful or effectful languages, incorporating (co)models of a countable Lawvere theory, have been elusive so far. We make some progress towards a coalgebraic treatment of such languages, proposing a congruence format related to the evaluation-in-context paradigm. We formalise the denotational semantics in suitable Kleisli categories, and prove adequacy and compositionality of the semantic theory under this congruence format.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Abou-Saleh, F., Pattinson, D.: Towards effects in mathematical operational semantics. Electr. Notes Theor. Comput. Sci. 276, 81–104 (2011)
Adamek, J.: Recursive data types in algebraically w-complete categories. Information and Computation 118(2), 181–190 (1995)
Adámek, J., Rosický, J.: Locally Presentable and Accessible Categories. Cambridge University Press (1994)
Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Logical Methods in Computer Science 3(4) (2007)
Hyland, M., Plotkin, G., Power, J.: Combining effects: sum and tensor. Theor. Comput. Sci. 357, 70–99 (2006)
Hyland, M., Power, J.: Discrete lawvere theories and computational effects. Theor. Comput. Sci. 366(1-2), 144–162 (2006)
Johann, P., Simpson, A., Voigtländer, J.: A generic operational metatheory for algebraic effects. In: Proc. LICS 2010, pp. 209–218. IEEE Computer Society (2010)
Kelly, G.M.: Basic concepts of enriched category theory. Reprints in Theory and Applications of Categories (10), 1–136 (2005)
Klin, B.: Bialgebraic methods in structural operational semantics. Electron. Notes Theor. Comput. Sci. 175(1), 33–43 (2007)
Kock, A.: Strong functors and monoidal monads. Archiv der Mathematik 23 (1972)
Lenisa, M., Power, J., Watanabe, H.: Category theory for operational semantics. Theor. Comput. Sci. 327(1-2), 135–154 (2004)
Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)
Monteiro, L.: A Coalgebraic Characterization of Behaviours in the Linear Time – Branching Time Spectrum. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 251–265. Springer, Heidelberg (2009)
Plotkin, G., Power, J.: Tensors of comodels and models for operational semantics. Electron. Notes Theor. Comput. Sci. 218, 295–311 (2008)
Plotkin, G.D., Power, J.: Adequacy for Algebraic Effects. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 1–24. Springer, Heidelberg (2001)
Plotkin, G., Power, J.: Notions of Computation Determine Monads. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 342–356. Springer, Heidelberg (2002)
Power, J.: Countable lawvere theories and computational effects. Electr. Notes Theor. Comput. Sci. 161, 59–71 (2006)
Power, J.: Semantics for local computational effects. Electr. Notes Theor. Comput. Sci. 158, 355–371 (2006)
Power, J., Shkaravska, O.: From comodels to coalgebras: State and arrays. Electron. Notes Theor. Comput. Sci. 106 (2004)
Power, J., Turi, D.: A coalgebraic foundation for linear time semantics. In: Category Theory and Computer Science. Elsevier (1999)
Staton, S.: Completeness for Algebraic Theories of Local State. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 48–63. Springer, Heidelberg (2010)
Turi, D.: Functorial Operational Semantics and its Denotational Dual. PhD thesis, Free University, Amsterdam (June 1996)
Turi, D.: Categorical modelling of structural operational rules: Case studies. In: Category Theory and Computer Science, pp. 127–146 (1997)
Turi, D., Plotkin, G.D.: Towards a mathematical operational semantics. In: LICS, pp. 280–291 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abou-Saleh, F., Pattinson, D. (2013). Comodels and Effects in Mathematical Operational Semantics. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37075-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-37075-5_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37074-8
Online ISBN: 978-3-642-37075-5
eBook Packages: Computer ScienceComputer Science (R0)