{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,11]],"date-time":"2026-02-11T18:15:52Z","timestamp":1770833752845,"version":"3.50.1"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T00:00:00Z","timestamp":1657843200000},"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":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2022,9,30]]},"abstract":"<jats:p>\n            Compositional methods are central to the verification of software systems. For concurrent and communicating systems, compositional techniques based on\n            <jats:italic>behavioural type systems<\/jats:italic>\n            have received much attention. By abstracting communication protocols as types, these type systems can statically check that channels in a program interact following a certain protocol\u2014whether messages are exchanged in the intended order.\n          <\/jats:p>\n          <jats:p>\n            In this article, we put on our coalgebraic spectacles to investigate\n            <jats:italic>session types<\/jats:italic>\n            , a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subtyping relations in terms of canonical coinductive presentations. In turn, this coinductive presentation enables us to derive a decidable type system with subtyping for the \u03c0-calculus, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective coincide with existing ones. We further apply to session coalgebras the coalgebraic approach to regular languages via the so-called rational fixed point, inspired by the trinity of automata, regular languages, and regular expressions with session coalgebras, rational fixed point, and session types, respectively. We establish a suitable restriction on session coalgebras that determines a similar trinity, and reveals the mismatch between usual session types and our syntax-free coalgebraic approach. Furthermore, we extend our coalgebraic approach to account for\n            <jats:italic>context-free<\/jats:italic>\n            session types, by equipping session coalgebras with a stack.\n          <\/jats:p>","DOI":"10.1145\/3527633","type":"journal-article","created":{"date-parts":[[2022,7,15]],"date-time":"2022-07-15T12:29:14Z","timestamp":1657888154000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Session Coalgebras: A Coalgebraic View on Regular and Context-free Session Types"],"prefix":"10.1145","volume":"44","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8826-9607","authenticated-orcid":false,"given":"Alex C.","family":"Keizer","sequence":"first","affiliation":[{"name":"Master of Logic, ILLC, University of Amsterdam, The Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7610-8331","authenticated-orcid":false,"given":"Henning","family":"Basold","sequence":"additional","affiliation":[{"name":"LIACS\u2013Leiden University, Leiden, The Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1452-6180","authenticated-orcid":false,"given":"Jorge A.","family":"P\u00e9rez","sequence":"additional","affiliation":[{"name":"University of Groningen, Groningen, The Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2022,7,15]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"Ji\u0159\u00ed Ad\u00e1mek Stefan Milius and Lawrence S. Moss. 2021. Initial Algebras Terminal Coalgebras and the Theory of Fixed Points of Functors. Retrieved from http:\/\/www.stefan-milius.eu."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005706"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511600579"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/2060081"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(2:10)2016"},{"key":"e_1_3_2_9_2","volume-title":"Handbook of Categorical Algebra: Volume 1, Basic Category Theory","author":"Borceux Francis","year":"2008","unstructured":"Francis Borceux. 2008. Handbook of Categorical Algebra: Volume 1, Basic Category Theory. Cambridge University Press."},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77351-1_4"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/11841197_10"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538917.1538920"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000188"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_7"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_10"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_18"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CALCO.2015.86"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_19"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22944-2_13"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004112000394"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2629609"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_5"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.314.3"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44602-7_21"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.07.006"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.022"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_14"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/11548133_16"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.034"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(4:10)2016"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29834-9_2"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.11"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.09.017"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.014"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43376-8_10"},{"key":"e_1_3_2_48_2","unstructured":"Paolo Perrone. 2021. Notes on Category Theory with Examples from Basic Mathematics. Retrieved from https:\/\/arxiv:1912.10642."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_3_2_51_2","volume-title":"The Method of Coalgebra: Exercises in Coinduction","author":"Rutten Jan","year":"2019","unstructured":"Jan Rutten. 2019. The Method of Coalgebra: Exercises in Coinduction. CWI, Amsterdam. Retrieved from http:\/\/persistent-identifier.org\/?identifier=urn:nbn:nl:ui:18-28550."},{"key":"e_1_3_2_52_2","volume-title":"The Pi-Calculus\u2014A Theory of Mobile Processes","author":"Sangiorgi Davide","year":"2001","unstructured":"Davide Sangiorgi and David Walker. 2001. The Pi-Calculus\u2014A Theory of Mobile Processes. Cambridge University Press."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.023"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(1:13)2011"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048122"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951926"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31175-9_7"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2006.12.001"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.009"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527633","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527633","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527633"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,15]]},"references-count":62,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2022,9,30]]}},"alternative-id":["10.1145\/3527633"],"URL":"https:\/\/doi.org\/10.1145\/3527633","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,15]]},"assertion":[{"value":"2021-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}