{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T16:09:39Z","timestamp":1787069379008,"version":"build-2736575974"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["527481841, 531706730, and 517924115"],"award-info":[{"award-number":["527481841, 531706730, and 517924115"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>\n                    Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is\n                    <jats:italic toggle=\"yes\">compositionality<\/jats:italic>\n                    , guaranteeing that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilitate compositionality proofs and avoid boilerplate work, one would hope to employ the abstract bialgebraic methods provided by Turi and Plotkin's powerful theory of\n                    <jats:italic toggle=\"yes\">mathematical operational semantics<\/jats:italic>\n                    (a.k.a.\n                    <jats:italic toggle=\"yes\">abstract GSOS<\/jats:italic>\n                    ) or its recent extension by Goncharov et al. to higher-order languages. However, multiple attempts to apply abstract GSOS to stateful languages have thus failed. We propose a novel approach to the operational semantics of stateful languages based on the formal distinction between\n                    <jats:italic toggle=\"yes\">readers<\/jats:italic>\n                    (terms that expect an initial input store before being executed), and\n                    <jats:italic toggle=\"yes\">writers<\/jats:italic>\n                    (running terms that have already been provided with a store). In contrast to earlier work, this style of semantics is fully compatible with abstract GSOS, and we can thus leverage the existing theory to obtain coinductive reasoning techniques. We demonstrate that our approach generates non-trivial compositionality results for stateful languages with first-order and higher-order store and that it flexibly applies to program equivalences at different levels of granularity, such as trace, cost, and natural equivalence.\n                  <\/jats:p>","DOI":"10.1145\/3747513","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"246-275","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Bialgebraic Reasoning on Stateful Languages"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6924-8766","authenticated-orcid":false,"given":"Sergey","family":"Goncharov","sequence":"first","affiliation":[{"name":"Birmingham University, Birmingham, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2021-1644","authenticated-orcid":false,"given":"Stefan","family":"Milius","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander University Erlangen-N\u00fcrnberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander University Erlangen-N\u00fcrnberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8981-2328","authenticated-orcid":false,"given":"Stelios","family":"Tsampas","sequence":"additional","affiliation":[{"name":"University of Southern Denmark, Odense, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3265-7168","authenticated-orcid":false,"given":"Henning","family":"Urbat","sequence":"additional","affiliation":[{"name":"Friedrich-Alexander University Erlangen-N\u00fcrnberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.016"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_9"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158153"},{"key":"e_1_3_2_6_2","volume-title":"Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010","author":"Ahmed Amal","year":"2010","unstructured":"Amal Ahmed, Nick Benton, Lars Birkedal, and Martin Hofmann (Eds.). 2010. Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010. Dagstuhl Seminar Proceedings, Vol. 10351. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany. http:\/\/drops.dagstuhl.de\/portals\/10351\/"},{"key":"e_1_3_2_7_2","volume-title":"Types, Logics and Semantics for State, 03.02. - 08.02.2008","author":"Ahmed Amal","year":"2008","unstructured":"Amal Ahmed, Nick Benton, Martin Hofmann, and Greg Morrisett (Eds.). 2008. Types, Logics and Semantics for State, 03.02. - 08.02.2008. Dagstuhl Seminar Proceedings, Vol. 08061. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany. http:\/\/drops.dagstuhl.de\/portals\/08061\/"},{"key":"e_1_3_2_8_2","unstructured":"Amal Jamil Ahmed. 2004. Semantics of types for mutable state. Ph. D. Dissertation. USA. AAI3136691."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01111838"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926401"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00152-9"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Filippo Bonchi Daniela Petrisan Damien Pous and Jurriaan Rot. 2015. Lax Bialgebras and Up-To Techniques for Weak Bisimulations. In 26th International Conference on Concurrency Theory CONCUR 2015 Madrid Spain September 1-4 2015. 240\u2013253. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.240 10.4230\/LIPIcs.CONCUR.2015.240","DOI":"10.4230\/LIPIcs.CONCUR.2015.240"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.30"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571215"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Sergey Goncharov Stefan Milius Lutz Schr\u00f6der Stelios Tsampas and Henning Urbat. 2025. Bialgebraic Reasoning on Stateful Languages. CoRR abs\/2503.10955 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2503.10955 10.48550\/arXiv.2503.10955 arXiv:2503.10955","DOI":"10.48550\/arXiv.2503.10955"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90120-1"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39174"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3022670.2951943"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.08.002"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_2_30_2","unstructured":"Paul Blain Levy. 2001. Call-by-push-value. Ph. D. Dissertation. Queen Mary University of London UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.369233"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000125"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_2_35_2","first-page":"227","volume-title":"Higher Order Operational Techniques in Semantics","author":"Pitts Andrew M.","year":"1998","unstructured":"Andrew M. Pitts and Ian D. B. Stark. 1998. Operational Reasoning for Functions with Local State. In Higher Order Operational Techniques in Semantics, Andrew D. Gordon and Andrew M. Pitts (Eds.). Cambridge University Press, New York, NY, USA, 227\u2013274."},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_108"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Jonathan Sterling Daniel Gratzer and Lars Birkedal. 2022. Denotational semantics of general store and polymorphism. CoRR abs\/2210.02169 (2022). https:\/\/doi.org\/10.48550\/arXiv.2210.02169 10.48550\/arXiv.2210.02169 arXiv:2210.02169","DOI":"10.48550\/arXiv.2210.02169"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010022312623"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Daniele Turi and Gordon D. Plotkin. 1997. Towards a Mathematical Operational Semantics. In 12th Annual IEEE Symposium on Logic in Computer Science (LICS 1997) 280\u2013291. https:\/\/doi.org\/10.1109\/LICS.1997.614955 10.1109\/LICS.1997.614955","DOI":"10.1109\/LICS.1997.614955"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175706"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","unstructured":"Henning Urbat Stelios Tsampas Sergey Goncharov Stefan Milius and Lutz Schr\u00f6der. 2023. Weak Similarity in Higher-Order Mathematical Operational Semantics. arXiv:2302.08200 [cs.PL].","DOI":"10.1109\/LICS56636.2023.10175706"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.036"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:2)2008"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747513","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:00:23Z","timestamp":1784196023000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747513"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":48,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747513"],"URL":"https:\/\/doi.org\/10.1145\/3747513","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}