{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:29:02Z","timestamp":1770287342167,"version":"3.49.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1521539"],"award-info":[{"award-number":["1521539"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2930"],"award-info":[{"award-number":["N00014-17-1-2930"]}],"id":[{"id":"10.13039\/100000006","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":[[2022,8,29]]},"abstract":"<jats:p>\n            Monadic computations built by interpreting, or\n            <jats:italic>handling<\/jats:italic>\n            , operations of a  \n free monad are a compelling formalism for modeling language semantics and  \n defining the behaviors of effectful systems.  \n The resulting layered semantics offer the promise of modular reasoning principles  \n based on the equational theory of the underlying monads.  \n However, there are a number of obstacles to using such layered  \n interpreters in practice. With more layers comes more boilerplate and glue  \n code needed to define the monads and interpreters involved. That overhead is  \n compounded by the need to define and justify the relational reasoning  \n principles that characterize the equivalences at each layer.  \n  \n This paper addresses these problems by significantly extending the  \n capabilities of the Coq\n            <jats:italic>interaction trees<\/jats:italic>\n            (ITrees) library, which  \n supports layered monadic interpreters. We characterize a rich class of\n            <jats:italic>interpretable monads<\/jats:italic>\n            ---obtained by applying monad transformers to  \n ITrees---and show how to generically lift interpreters through them. We  \n also introduce a corresponding framework for relational reasoning about  \n \"equivalence of monads up to a relation R\". This collection of  \n typeclasses, instances, new reasoning principles, and tactics greatly  \n generalizes the existing theory of the ITree library, eliminating large  \n amounts of unwieldy boilerplate code and dramatically simplifying proofs.\n          <\/jats:p>","DOI":"10.1145\/3547630","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"254-282","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal reasoning about layered monadic interpreters"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3388-1257","authenticated-orcid":false,"given":"Irene","family":"Yoon","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4585-6470","authenticated-orcid":false,"given":"Yannick","family":"Zakowski","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3516-1512","authenticated-orcid":false,"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009878"},{"key":"e_1_2_1_3_1","unstructured":"Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. USA. AAI3136691 \t\t\t\t  Amal Jamil Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. USA. AAI3136691"},{"key":"e_1_2_1_4_1","volume-title":"Issue 15","author":"Apfelmus Heinrich","year":"2010","unstructured":"Heinrich Apfelmus . 2010. The Operational Monad Tutorial. The Monad.Reader , Issue 15 ( 2010 ). Heinrich Apfelmus. 2010. The Operational Monad Tutorial. The Monad.Reader, Issue 15 (2010)."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40206-7_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599447"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-78034-9"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508007172"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_21"},{"key":"e_1_2_1_15_1","volume-title":"Bisimulation as a Logical Relation. CoRR, abs\/2003.13542","author":"Hermida Claudio","year":"2020","unstructured":"Claudio Hermida , Uday S. Reddy , Edmund P. Robinson , and Alessio Santamaria . 2020. Bisimulation as a Logical Relation. CoRR, abs\/2003.13542 ( 2020 ), arXiv:2003.13542. arxiv:2003.13542 Claudio Hermida, Uday S. Reddy, Edmund P. Robinson, and Alessio Santamaria. 2020. Bisimulation as a Logical Relation. CoRR, abs\/2003.13542 (2020), arXiv:2003.13542. arxiv:2003.13542"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-009-9047-7"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2887747.2804319"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503791"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005117"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_20"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547632"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61055-3_39"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341708"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19797-5_13"},{"key":"e_1_2_1_31_1","volume-title":"Foundations for Programming Languages","author":"Mitchell John C.","unstructured":"John C. Mitchell . 1996. Foundations for Programming Languages . The MIT Press . John C. Mitchell. 1996. Foundations for Programming Languages. The MIT Press."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_1_33_1","volume-title":"An Abstract View of Programming Languages. Laboratory for the Foundations of Computer Science","author":"Moggi Eugenio","unstructured":"Eugenio Moggi . 1990. An Abstract View of Programming Languages. Laboratory for the Foundations of Computer Science , University of Edinburgh. Eugenio Moggi. 1990. An Abstract View of Programming Languages. Laboratory for the Foundations of Computer Science, University of Edinburgh."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.015"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_1_41_1","volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi Davide","unstructured":"Davide Sangiorgi . 2012. Introduction to Bisimulation and Coinduction ( 2 nd ed.). Cambridge University Press , USA. isbn:9781107003637 Davide Sangiorgi. 2012. Introduction to Bisimulation and Coinduction (2nd ed.). Cambridge University Press, USA. isbn:9781107003637","edition":"2"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000119"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178068"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341707"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91592"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6913915"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_3"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103709"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547630","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547630","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547630","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547630"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":52,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547630"],"URL":"https:\/\/doi.org\/10.1145\/3547630","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}