{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:31:36Z","timestamp":1750221096201,"version":"3.41.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We propose a categorical framework for structural operational semantics, in which we prove that under suitable hypotheses bisimilarity is a congruence. We then refine the framework to prove soundness of bisimulation up to context, an efficient method for reducing the size of bisimulation relations. Finally, we demonstrate the flexibility of our approach by reproving known results in three variants of the \u03c0-calculus.<\/jats:p>","DOI":"10.1145\/3290334","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Familial monads and structural operational semantics"],"prefix":"10.1145","volume":"3","author":[{"given":"Tom","family":"Hirschowitz","sequence":"first","affiliation":[{"name":"Grenoble Alps University, France \/ Savoie Mont Blanc University, France \/ CNRS, France \/ LAMA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"key-10.1145\/3290334-1","doi-asserted-by":"crossref","unstructured":"C. Berger, P.-A. Melli&#232;s, and M. Weber. 2012. Monads with arities and their associated theories. Journal of Pure and Applied Algebra 216, 8 (2012), 2029 &#8211; 2048.","DOI":"10.1016\/j.jpaa.2012.02.039"},{"key":"key-10.1145\/3290334-2","doi-asserted-by":"crossref","unstructured":"Karen L. Bernstein. 1998. A Congruence Theorem for Structured Operational Semantics of Higher-Order Languages. In Proc. 13th Symposium on Logic in Computer Science IEEE Computer Society, 153&#8211;164.","DOI":"10.1109\/LICS.1998.705652"},{"key":"key-10.1145\/3290334-3","doi-asserted-by":"crossref","unstructured":"Bard Bloom, Sorin Istrail, and Albert R. Meyer. 1995. Bisimulation Can&#8217;t be Traced. Journal of the ACM 42, 1 (1995), 232&#8211;268.","DOI":"10.1145\/200836.200876"},{"key":"key-10.1145\/3290334-4","doi-asserted-by":"crossref","unstructured":"Roland N. Bol and Jan Friso Groote. 1996. The Meaning of Negative Premises in Transition System Specifications. Journal of the ACM 43, 5 (1996), 863&#8211;914.","DOI":"10.1145\/234752.234756"},{"key":"key-10.1145\/3290334-5","unstructured":"Filippo Bonchi, Daniela Petri&#351;an, Damien Pous, and Jurriaan Rot. 2016. A general account of coinduction up-to. Acta Informatica (2016), 1&#8211;64."},{"key":"key-10.1145\/3290334-6","doi-asserted-by":"crossref","unstructured":"G&#233;rard Boudol and Ilaria Castellani. 1988. A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae XI (1988).","DOI":"10.3233\/FI-1988-11406"},{"key":"key-10.1145\/3290334-7","doi-asserted-by":"crossref","unstructured":"Aurelio Carboni and Peter Johnstone. 1995. Connected limits, familial representability and Artin glueing. Mathematical Structures in Computer Science 5, 4 (1995), 441&#8211;459.","DOI":"10.1017\/S0960129500001183"},{"key":"key-10.1145\/3290334-8","unstructured":"Gian Luca Cattani, John Power, and Glynn Winskel. 1998. A Categorical Axiomatics for Bisimulation, See [ Sangiorgi and de Simone 1998 ], 581&#8211;596."},{"key":"key-10.1145\/3290334-9","unstructured":"Yves Diers. 1978. Spectres et localisations relatifs &#224; un foncteur. Comptes rendus hebdomadaires des s&#233;ances de l&#8217;Acad&#233;mie des sciences 287, 15 (1978), 985&#8211;988."},{"key":"key-10.1145\/3290334-10","unstructured":"J&#233;r&#233;my Dubut, Eric Goubault, and Jean Goubault-Larrecq. 2016. Bisimulations and unfolding in &#119979;-accessible categorical models. In Proc. 27th International Conference on Concurrency Theory (LIPIcs), Jos&#233;e Desharnais and Radha Jagadeesan (Eds.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik."},{"key":"key-10.1145\/3290334-11","doi-asserted-by":"crossref","unstructured":"Marcelo P. Fiore and Sam Staton. 2006. A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics. In Proc. 21st Symposium on Logic in Computer Science IEEE, 49&#8211;58.","DOI":"10.1109\/LICS.2006.7"},{"key":"key-10.1145\/3290334-12","unstructured":"Marcelo P. Fiore and Daniele Turi. 2001. Semantics of Name and Value Passing. In Proc. 16th Symposium on Logic in Computer Science IEEE, 93&#8211;104."},{"key":"key-10.1145\/3290334-13","doi-asserted-by":"crossref","unstructured":"Richard H. G. Garner and Tom Hirschowitz. 2018. Shapely monads and analytic functors. Journal of Logic and Computation 28, 1 (2018), 33&#8211;83.","DOI":"10.1093\/logcom\/exx029"},{"key":"key-10.1145\/3290334-14","unstructured":"Tom Hirschowitz. 2018. Familial monads and structural operational semantics. (2018). https:\/\/hal.archives-ouvertes.fr\/ hal-01815328 Preprint."},{"key":"key-10.1145\/3290334-15","unstructured":"Mark Hovey. 1999. Model Categories. Mathematical Surveys and Monographs, Volume 63, AMS (1999), Vol. 63. American Mathematical Society."},{"key":"key-10.1145\/3290334-16","doi-asserted-by":"crossref","unstructured":"Peter T. Johnstone. 2002. Sketches of an Elephant: A Topos Theory Compendium - Volume 1. Oxford University Press.","DOI":"10.1093\/oso\/9780198515982.003.0004"},{"key":"key-10.1145\/3290334-17","doi-asserted-by":"crossref","unstructured":"Andr&#233; Joyal, Mogens Nielsen, and Glynn Winskel. 1993. Bisimulation and open maps. In Proc. 8th Symposium on Logic in Computer Science IEEE, 418&#8211;427.","DOI":"10.1109\/LICS.1993.287566"},{"key":"key-10.1145\/3290334-18","doi-asserted-by":"crossref","unstructured":"Bartek Klin. 2011. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science 412, 38 (2011), 5043&#8211;5069.","DOI":"10.1016\/j.tcs.2011.03.023"},{"key":"key-10.1145\/3290334-19","unstructured":"Joachim Kock. 2011. Polynomial functors and trees. International Mathematics Research Notices 2011, 3 (2011), 609&#8211;673."},{"key":"key-10.1145\/3290334-20","doi-asserted-by":"crossref","unstructured":"F. W. Lawvere. 1963. Functorial semantics of algebraic theories. Ph.D. Dissertation. Columbia University.","DOI":"10.1073\/pnas.50.5.869"},{"key":"key-10.1145\/3290334-21","unstructured":"Saunders Mac Lane. 1998. Categories for the Working Mathematician (2nd ed.). Number 5 in Graduate Texts in Mathematics. Springer."},{"key":"key-10.1145\/3290334-22","unstructured":"Saunders Mac Lane and Ieke Moerdijk. 1992. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer."},{"key":"key-10.1145\/3290334-23","doi-asserted-by":"crossref","unstructured":"C. A. Middelburg. 2001. Variable binding operators in transition system specifications. Journal of Logic and Algebraic Programming 47, 1 (2001), 15&#8211;45.","DOI":"10.1016\/S1567-8326(00)00003-5"},{"key":"key-10.1145\/3290334-24","unstructured":"MohammadReza Mousavi, Michel A. Reniers, and Jan Friso Groote. 2007. SOS Formats and Meta-Theory: 20 Years After. Theoretical Computer Science 373, 3 (2007), 238&#8211;272."},{"key":"key-10.1145\/3290334-25","doi-asserted-by":"crossref","unstructured":"Mohammad Reza Mousavi, Murdoch Gabbay, and Michel A. Reniers. 2005. SOS for Higher Order Processes. In CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings (Lecture Notes in Computer Science), Mart&#237;n Abadi and Luca de Alfaro (Eds.), Vol. 3653. Springer, 308&#8211;322.","DOI":"10.1007\/11539452_25"},{"key":"key-10.1145\/3290334-26","unstructured":"Gordon D. Plotkin. 1981. A Structural Approach to Operational Semantics. DAIMI Report FN-19. Computer Science Department, Aarhus University."},{"key":"key-10.1145\/3290334-27","doi-asserted-by":"crossref","unstructured":"Damien Pous and Davide Sangiorgi. 2011. Enhancements of the bisimulation proof method, Chapter 6. In Sangiorgi and Rutten [ Sangiorgi and Rutten 2011 ].","DOI":"10.1017\/CBO9780511792588.007"},{"key":"key-10.1145\/3290334-28","doi-asserted-by":"crossref","unstructured":"Emily Riehl. 2014. Categorical Homotopy Theory. Number 24 in New Mathematical Monographs. Cambridge University Press.","DOI":"10.1017\/CBO9781107261457"},{"key":"key-10.1145\/3290334-29","doi-asserted-by":"crossref","unstructured":"David Sands. 1997. From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages. In Proc. 24th International Symposium on Principles of Programming Languages, Peter Lee, Fritz Henglein, and Neil D. Jones (Eds.). ACM Press, 428&#8211;441.","DOI":"10.1145\/263699.263760"},{"key":"key-10.1145\/3290334-30","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi. 1994. The Lazy Lambda Calculus in a Concurrency Scenario. Information and Computation 111, 1 (1994), 120&#8211;153.","DOI":"10.1006\/inco.1994.1042"},{"key":"key-10.1145\/3290334-31","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi and Robert de Simone (Eds.). 1998. Proc. 9th International Conference on Concurrency Theory. LNCS, Vol. 1466. Springer.","DOI":"10.1007\/BFb0055611"},{"key":"key-10.1145\/3290334-32","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi and Jan Rutten (Eds.). 2011. Advanced Topics in Bisimulation and Coinduction. Number 52 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.","DOI":"10.1017\/CBO9780511792588"},{"key":"key-10.1145\/3290334-33","unstructured":"Davide Sangiorgi and David Walker. 2001. The &#120587;-calculus &#8211; A Theory of Mobile Processes. Cambridge University Press."},{"key":"key-10.1145\/3290334-34","unstructured":"Peter Sewell. 1998. From Rewrite Rules to Bisimulation Congruences, See [ Sangiorgi and de Simone 1998 ], 269&#8211;284."},{"key":"key-10.1145\/3290334-35","doi-asserted-by":"crossref","unstructured":"Sam Staton. 2008. General Structural Operational Semantics through Categorical Logic. In Proc. 23rd Symposium on Logic in Computer Science 166&#8211;177.","DOI":"10.1109\/LICS.2008.43"},{"key":"key-10.1145\/3290334-36","doi-asserted-by":"crossref","unstructured":"Daniele Turi and Gordon D. Plotkin. 1997. Towards a Mathematical Operational Semantics. In Proc. 12th Symposium on Logic in Computer Science 280&#8211;291.","DOI":"10.1109\/LICS.1997.614955"},{"key":"key-10.1145\/3290334-37","unstructured":"Mark Weber. 2007. Familial 2-functors and parametric right adjoints. Theory and Applications of Categories 18, 22 (2007), 665&#8211;732."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290334","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290334","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290334"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290334"],"URL":"https:\/\/doi.org\/10.1145\/3290334","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}