{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:27:50Z","timestamp":1755217670738,"version":"3.43.0"},"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>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 compositionality, 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\u2019s powerful theory of mathematical operational semantics (a.k.a. abstract GSOS) 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 readers (terms that expect an initial input store before being executed), and writers (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.<\/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":0,"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"}]},{"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"}]},{"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"}]},{"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"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.016"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_9"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158153"},{"key":"e_1_2_1_5_1","first-page":"08","article-title":"Modelling","volume":"29","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\/","journal-title":"Controlling and Reasoning About State"},{"key":"e_1_2_1_6_1","first-page":"02","article-title":"Types","volume":"03","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\/","journal-title":"Logics and Semantics for State"},{"key":"e_1_2_1_7_1","unstructured":"Amal Jamil Ahmed. 2004. Semantics of types for mutable state. Ph. D. Dissertation. USA. AAI3136691"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01111838"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926401"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00152-9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2015.240"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.30"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571215"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2503.10955"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90120-1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2725"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39174"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022670.2951943"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.08.002"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_1_29_1","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"},{"volume-title":"Categories for the Working Mathematician (2 ed.) (Graduate Texts in Mathematics","author":"Lane S. Mac","key":"e_1_2_1_30_1","unstructured":"S. Mac Lane. 1978. Categories for the Working Mathematician (2 ed.) (Graduate Texts in Mathematics, Vol. 5). Springer. http:\/\/link.springer.com\/10.1007\/978-1-4757-4721-8"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000125"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"volume-title":"Types and programming languages","author":"Pierce Benjamin C.","key":"e_1_2_1_33_1","unstructured":"Benjamin C. Pierce. 2002. Types and programming languages. MIT Press."},{"key":"e_1_2_1_34_1","volume-title":"Stark","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_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_108"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2210.02169"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010022312623"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614955"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175706"},{"key":"e_1_2_1_44_1","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.","DOI":"10.1109\/LICS56636.2023.10175706"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.036"},{"volume-title":"The formal semantics of programming languages: an introduction","author":"Winskel Glynn","key":"e_1_2_1_47_1","unstructured":"Glynn Winskel. 1993. The formal semantics of programming languages: an introduction. MIT press."},{"key":"e_1_2_1_48_1","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":[[2025,8,5]],"date-time":"2025-08-05T16:56:45Z","timestamp":1754413005000},"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":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}