{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,2]],"date-time":"2026-02-02T14:19:55Z","timestamp":1770041995559,"version":"3.49.0"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            This paper presents a novel formalisation of algebraic effects with equations in Cubical Agda. Unlike previous work in the literature that employed\n            <jats:italic toggle=\"yes\">setoids<\/jats:italic>\n            to deal with equations, the library presented here uses quotient types to faithfully encode the type of terms quotiented by laws. Apart from tools for equational reasoning, the library also provides an\n            <jats:italic toggle=\"yes\">effect-generic Hoare logic<\/jats:italic>\n            for algebraic effects, which enables reasoning about effectful programs in terms of their pre- and post-conditions. A particularly novel aspect is that equational reasoning and Hoare-style reasoning are related by an elimination principle of Hoare logic.\n          <\/jats:p>","DOI":"10.1145\/3632898","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1663-1695","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Algebraic Effects Meet Hoare Logic in Cubical Agda"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4952-7359","authenticated-orcid":false,"given":"Donnacha Ois\u00edn","family":"Kidney","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5573-3357","authenticated-orcid":false,"given":"Zhixuan","family":"Yang","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4161-985X","authenticated-orcid":false,"given":"Nicolas","family":"Wu","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Andreas Abel. 2021. Birkhoff\u2019s Completeness Theorem for Multi-Sorted Algebras Formalized in Agda. https:\/\/doi.org\/10.48550\/arXiv.2111.07936 10.48550\/arXiv.2111.07936 arXiv:2111.07936 [cs]","DOI":"10.48550\/arXiv.2111.07936"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00728-4"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.09.002"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158095"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000347"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3006383"},{"key":"e_1_3_1_9_1","article-title":"What Is Algebraic about Algebraic Effects and Handlers?arXiv:1807.05923 [cs] (March 2019)","author":"Bauer Andrej","year":"2019","unstructured":"Andrej Bauer. 2019. What Is Algebraic about Algebraic Effects and Handlers?arXiv:1807.05923 [cs] (March 2019). arXiv:1807.05923 [cs] http:\/\/arxiv.org\/abs\/1807.05923","journal-title":"arXiv:1807.05923"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_1"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3533359"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158096"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100013463"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61667-9"},{"key":"e_1_3_1_15_1","first-page":"20\u201335","volume-title":"Foundations of Software Science and Computation Structures","author":"Bizjak Ale\u0161","year":"2016","unstructured":"Ale\u0161 Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. M\u00f8gelberg, Lars Birkedal. 2016. Guarded Dependent Type Theory with Coinductive Types. In Foundations of Software Science and Computation Structures, Bart Jacobs and Christof L\u00f6ding (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 20\u201335."},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276481"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_10"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-8399-1"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005130"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2021.28"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2021.4"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(2:15)2022"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167085"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563445"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034777"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.33"},{"key":"e_1_3_1_30_1","unstructured":"Daniel Gratzer Jonathan Sterling Carlo Angiuli Thierry Coquand and Lars Birkedal. 2022. Controlling unfolding in type theory. https:\/\/doi.org\/arXiv.2210.05420 arXiv:2210.05420 [cs.LO]"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.010"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.047"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003050"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.026"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(93)90092-8"},{"key":"e_1_3_1_38_1","volume-title":"Finiteness in Cubical Type Theory","author":"Kidney Donnacha Ois\u00edn","year":"2020","unstructured":"Donnacha Ois\u00edn Kidney. 2020. Finiteness in Cubical Type Theory. MRes Thesis. University College Cork, Cork, Ireland. https:\/\/cora.ucc.ie\/handle\/10468\/11338"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","unstructured":"Donnacha Oisin Kidney Zhixuan Yang and Nicolas Wu. 2023. Artefact for Algebraic Effects Meet Hoare Logic in Cubical Agda. https:\/\/doi.org\/10.5281\/zenodo.8422532 10.5281\/zenodo.8422532","DOI":"10.5281\/zenodo.8422532"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547632"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_3_1_45_1","first-page":"153","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Martin-L\u00f6f Per","year":"1982","unstructured":"Per Martin-L\u00f6f. 1982. Constructive Mathematics and Computer Programming. In Studies in Logic and the Foundations of Mathematics. Vol. 104. North-Holland Publishing Company, 153\u2013175. https:\/\/doi.org\/10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_1_46_1","first-page":"51","volume-title":"An Abstract View of Programming Languages","author":"Moggi Eugenio","year":"1989","unstructured":"Eugenio Moggi. 1989. An Abstract View of Programming Languages. Technical Report ECS-LFCS-90-113. University of Edinburgh. 51 pages. http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/90\/ECS-LFCS-90-113\/"},{"key":"e_1_3_1_47_1","first-page":"55","volume-title":"Information and Computation","author":"Moggi Eugenio","year":"1991","unstructured":"Eugenio Moggi. 1991. Notions of Computation and Monads. Information and Computation 93, 1 (July 1991), 55\u201392. https:\/\/doi.org\/10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209166"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.008"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:9)2014"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_57_1","unstructured":"Egbert Rijke Elisabeth Bonnevier Jonathan Prieto-Cubides Fredrik Bakke . 2021. The Agda-Unimath Library. https:\/\/github.com\/UniMath\/agda-unimath\/"},{"key":"e_1_3_1_58_1","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-031-16912-0_6","volume-title":"Mathematics of Program Construction","author":"Saito Ayumu","year":"2022","unstructured":"Ayumu Saito and Reynald Affeldt. 2022. Towards a Practical Library for Monadic Equational Reasoning in Coq. In Mathematics of Program Construction, Ekaterina Komendantskaya (Ed.). Springer International Publishing, Cham, 151\u2013177."},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45719-4_8"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36578-8_19"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523710"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408975"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434307"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454039"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.58"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676999"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209153"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2491978"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_1_72_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"The Univalent Foundations Program","year":"2013","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study."},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_11"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_17"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607850"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547630"},{"key":"e_1_3_1_80_1","volume-title":"Combinatorial Species and Labelled Structures","author":"Yorgey Brent A.","year":"2014","unstructured":"Brent A. Yorgey. 2014. Combinatorial Species and Labelled Structures. Ph. D. Dissertation. University of Pennsylvania, Pennsylvania. https:\/\/repository.upenn.edu\/dissertations\/AAI3668177"},{"key":"e_1_3_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290318"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632898","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632898","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:08Z","timestamp":1751659448000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632898"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":80,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632898"],"URL":"https:\/\/doi.org\/10.1145\/3632898","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}