{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:32Z","timestamp":1787592272800,"version":"build-2736575974"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>This paper proves an adequacy theorem for a general class of algebraic effects, including infinitary ones. The theorem targets a version of Call-by-Push-Value (CBPV), so that it applies to many possible evaluation mechanisms, including call-by-value. The calculus is given an operational semantics based on interaction trees, as well as a denotational semantics based on monad algebras. The main result, viz. that denotational equivalence implies observational equivalence, using a traditional logical relations argument.<\/jats:p>","DOI":"10.1145\/3720457","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"927-955","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Adequacy for Algebraic Effects Revisited"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7953-7975","authenticated-orcid":false,"given":"G. A.","family":"Kavvos","sequence":"first","affiliation":[{"name":"University of Bristol, School of Computer Science, Bristol, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003054"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:2)2010"},{"key":"e_1_3_2_4_1","first-page":"1","volume-title":"Handbook of Logic in Computer Science","author":"Abramsky Samson","year":"1994","unstructured":"Samson Abramsky and Achim Jung. 1994. \u201cDomain Theory.\u201d In: Handbook of Logic in Computer Science. Vol. 3. Ed. by Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum. Oxford University Press, 1\u2013168. https:\/\/www.cs.bham.ac.uk\/~axj\/pub\/papers\/handy1.pdf."},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0060439"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2828"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_99"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-8399-1"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-20(2:1)2024"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498692"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_10"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.12.025"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_3_2_17_1","volume-title":"PhD thesis","author":"Gavazzo Francesco","year":"2019","unstructured":"Francesco Gavazzo. 2019. \u201cCoinductive Equivalences and Metrics for Higher-order Languages with Algebraic Effects.\u201d PhD thesis. Universit\u00e0 di Bologna. https:\/\/theses.hal.science\/tel-02386201."},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_2"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.33"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00353-3"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_37"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","unstructured":"Jean Goubault-Larrecq S\u0142awomir Lasota and David Nowak. 2008. \u201cLogical relations for monadic types.\u201d Mathematical Structures in Computer Science 18 06 1169\u20131217. doi:10.1017\/S0960129508007172.","DOI":"10.1017\/S0960129508007172"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316576892"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/0209005"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09526-8_8"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90015-8"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15545-6_7"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498705"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103698"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_8"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.014"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(4:6)2018"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.08.002"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3537668.3537670"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0954-6"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_3"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.12.006"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.360.6"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(67)90353-1"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71948-7"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56992-8_21"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_48_1","volume-title":"\u201cLambda-calculus models of programming languages.\u201d PhD thesis","author":"Morris James Hiram","year":"1969","unstructured":"James Hiram Morris. 1969. \u201cLambda-calculus models of programming languages.\u201d PhD thesis. Massachusetts Institute of Technology. http:\/\/hdl.handle.net\/1721.1\/64850."},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198537809.003.0003"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_2_51_1","first-page":"197","volume-title":"Advanced Topics in Bisimulation and Coinduction. Cambridge Tracts in Theoretical Computer Science","author":"Pitts A. M.","year":"2011","unstructured":"A. M. Pitts. 2011. \u201cHowe\u2019s Method for Higher-Order Languages.\u201d In: Advanced Topics in Bisimulation and Coinduction. Cambridge Tracts in Theoretical Computer Science. Vol. 52. Ed. by D. Sangiorgi and J. Rutten. Cambridge University Press, 197\u2013232. https:\/\/www.cl.cam.ac.uk\/~amp12\/papers\/howmho\/howmho.pdf."},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.007"},{"key":"e_1_3_2_53_1","first-page":"227","volume-title":"Higher Order Operational Techniques in Semantics. Publications of the Newton Institute","author":"Pitts Andrew","year":"1998","unstructured":"Andrew Pitts and Ian Stark. 1998. \u201cOperational Reasoning for Functions with Local State.\u201d In: Higher Order Operational Techniques in Semantics. Publications of the Newton Institute. Ed. by A. D. Gordon and A. M. Pitts. Cambridge University Press, 227\u2013273. https:\/\/homepages.inf.ed.ac.uk\/stark\/operfl.pdf."},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03741-2_1"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_8"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_1"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.008"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_2_67_1","volume-title":"Doctoral thesis","author":"Schalk Andrea","year":"1993","unstructured":"Andrea Schalk. 1993. \u201cAlgebras for Generalized Power Constructions.\u201d Doctoral thesis. Technische Hochschule Darmstadt."},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037119"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_11"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363518"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0036946"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_26"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_5"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","unstructured":"Sam Staton. 2013b. \u201cInstances of Computational Effects: An Algebraic Perspective.\u201d In: 2013 28th Annual ACM\/IEEE Symposium on Logic in Computer Science. IEEE. doi:10.1109\/LICS.2013.58.","DOI":"10.1109\/LICS.2013.58"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/1212163"},{"key":"e_1_3_2_77_1","volume-title":"Ph.D. Dissertation","author":"Thijs Albert Marchienus","year":"1996","unstructured":"Albert Marchienus Thijs. 1996. \u201cSimulation and Fixpoint Semantics.\u201d Ph.D. Dissertation. University of Groningen. https:\/\/hdl.handle.net\/11370\/13d08025-29ff-4193-a7f2-ea5bcd20f15d."},{"key":"e_1_3_2_78_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720457","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720457","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:28:52Z","timestamp":1787588932000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720457"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":78,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720457"],"URL":"https:\/\/doi.org\/10.1145\/3720457","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}