{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:00:13Z","timestamp":1787061613391,"version":"build-2736575974"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["527481841,501369690,470467389"],"award-info":[{"award-number":["527481841,501369690,470467389"]}],"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,1,7]]},"abstract":"<jats:p>\n                    Levy\u2019s call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes both call-by-value and call-byname evaluation strategies. In the present work, we develop modular methods to reason about program equivalence in call-by-push-value, and in fine-grain call-by-value, which is a popular lightweight call-by-value sublanguage of the former. Our approach is based on the fundamental observation that presheaf categories of\n                    <jats:italic toggle=\"yes\">sorted sets<\/jats:italic>\n                    are suitable universes to model call-by-(push)-value languages, and that natural, coalgebraic notions of program equivalence such as applicative similarity and logical relations can be developed within. Starting from this observation, we formalize fine-grain call-by-value and call-by-push-value in the\n                    <jats:italic toggle=\"yes\">higher-order abstract GSOS<\/jats:italic>\n                    framework, reduce their key congruence properties to simple syntactic conditions by leveraging existing theory and argue that introducing changes to either language incurs minimal proof overhead.\n                  <\/jats:p>","DOI":"10.1145\/3704871","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1013-1039","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Abstract Operational Methods for Call-by-Push-Value"],"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":"University of Birmingham, Birmingham, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8981-2328","authenticated-orcid":false,"given":"Stelios","family":"Tsampas","sequence":"additional","affiliation":[{"name":"FAU Erlangen-Nuremberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3265-7168","authenticated-orcid":false,"given":"Henning","family":"Urbat","sequence":"additional","affiliation":[{"name":"FAU Erlangen-Nuremberg, Erlangen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","first-page":"65","volume-title":"Research topics in Functional Programming","author":"Abramsky S.","year":"1990","unstructured":"S. Abramsky . 1990. The lazy A-calculus. In Research topics in Functional Programming. Addison Wesley, 65-117."},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel and David A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23 5 (2001) 657-683. https:\/\/doi.org\/10.1145\/504709.504712 10.1145\/504709.504712","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2060081"},{"key":"e_1_3_2_5_1","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) (LIPIcs Vol. 42) Luca Aceto and David de Frutos-Escrig (Eds.). 240-253. 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_6_1","doi-asserted-by":"publisher","DOI":"10.2307\/2370619"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000263"},{"key":"e_1_3_2_8_1","unstructured":"Marcelo Fiore and Sam Staton. 2010. Positive structural operational semantics and monotone distributive laws. (2010). https:\/\/www.cs.ox.ac.uk\/people\/samuel.staton\/papers\/cmcs10.pdf."},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_26"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"Yannick Forster Steven Sch\u00e4fer Simon Spies and Kathrin Stark. 2019. Call-by-push-value in Coq: operational equational and denotational theory. In 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2019). ACM 118-131. https:\/\/doi.org\/10.1145\/3293880.3294097 10.1145\/3293880.3294097","DOI":"10.1145\/3293880.3294097"},{"key":"e_1_3_2_12_1","article-title":"Structural Operational Semantics for Control Flow Graph Machines","author":"Garbuzov Dmitri","year":"2018","unstructured":"Dmitri Garbuzov, William Mansky, Christine Rizkallah, and Steve Zdancewic. 2018. Structural Operational Semantics for Control Flow Graph Machines. CoRR (2018). arXiv:1805.05400","journal-title":"CoRR (2018)"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571215"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662099"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57231-9_3"},{"key":"e_1_3_2_16_1","doi-asserted-by":"crossref","unstructured":"Sergey Goncharov Stelios Tsampas and Henning Urbat. 2024c. Abstract Operational Methods for Call-by-Push-Value. arXiv:2410.17045 [cs.PL] https:\/\/doi.org\/10.1145\/3661814.3662099","DOI":"10.1145\/3704871"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:37)2022"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39174"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371083"},{"key":"e_1_3_2_22_1","volume-title":"Relational Reasoning about Functions and Nondeterminism","author":"Lassen. S\u00f8ren B.","year":"1998","unstructured":"S\u00f8ren B. Lassen. 1998. Relational Reasoning about Functions and Nondeterminism. Ph. D. Dissertation. Aarhus University. https:\/\/www.brics.dk\/DS\/98\/2\/BRICS-DS-98-2.pdf"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.15"},{"key":"e_1_3_2_24_1","volume-title":"Call-by-push-value","author":"Paul Blain Levy","year":"2001","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_25_1","doi-asserted-by":"publisher","unstructured":"Paul Blain Levy . 2022. Call-by-push-value. ACM SIGLOG News 9 2 (2022) 7-29. https:\/\/doi.org\/10.1145\/3537668.3537670 10.1145\/3537668.3537670","DOI":"10.1145\/3537668.3537670"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_9"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/237842"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_32_1","volume-title":"Lambda-Calculus Models of Programming Languages","author":"Morris James H.","year":"1968","unstructured":"James H. Morris . 1968. Lambda-Calculus Models of Programming Languages. Ph. D. Dissertation. Massachusetts Institute of Technology."},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.006"},{"key":"e_1_3_2_34_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts Andrew M.","year":"2004","unstructured":"Andrew M. Pitts . 2004. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). The MIT Press, Chapter 7."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_31"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614955"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175706"},{"key":"e_1_3_2_38_1","doi-asserted-by":"crossref","unstructured":"Henning Urbat Stelios Tsampas Sergey Goncharov Stefan Milius and Lutz Schr\u00f6der. 2023b. Weak Similarity in Higher-Order Mathematical Operational Semantics. arXiv:2302.08200 [cs.PL]","DOI":"10.1109\/LICS56636.2023.10175706"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704871","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704871","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:56Z","timestamp":1770200276000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704871"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704871"],"URL":"https:\/\/doi.org\/10.1145\/3704871","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}