{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:27:23Z","timestamp":1784255243521,"version":"3.55.0"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["2017R1A2B2007512"],"award-info":[{"award-number":["2017R1A2B2007512"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007297","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\/100007297","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1521602,1521539,1421243"],"award-info":[{"award-number":["1521602,1521539,1421243"]}],"id":[{"id":"10.13039\/100000001","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":[[2020,1]]},"abstract":"<jats:p>\n            <jats:italic>Interaction trees<\/jats:italic>\n            (ITrees) are a general-purpose data structure for representing the behaviors of recursive programs that interact with their environments. A coinductive variant of \u201cfree monads,\u201d ITrees are built out of uninterpreted events and their continuations. They support compositional construction of interpreters from\n            <jats:italic>event handlers<\/jats:italic>\n            , which give meaning to events by defining their semantics as monadic actions. ITrees are expressive enough to represent impure and potentially nonterminating, mutually recursive computations, while admitting a rich equational theory of equivalence up to weak bisimulation. In contrast to other approaches such as relationally specified operational semantics, ITrees are executable via code extraction, making them suitable for debugging, testing, and implementing software artifacts that are amenable to formal verification.\n          <\/jats:p>\n          <jats:p>We have implemented ITrees and their associated theory as a Coq library, mechanizing classic domain- and category-theoretic results about program semantics, iteration, monadic structures, and equational reasoning. Although the internals of the library rely heavily on coinductive proofs, the interface hides these details so that clients can use and reason about ITrees without explicit use of Coq\u2019s coinduction tactics.<\/jats:p>\n          <jats:p>To showcase the utility of our theory, we prove the termination-sensitive correctness of a compiler from a simple imperative source language to an assembly-like target whose meanings are given in an ITree-based denotational semantics. Unlike previous results using operational techniques, our bisimulation proof follows straightforwardly by structural induction and elementary rewriting via an equational theory of combinators for control-flow graphs.<\/jats:p>","DOI":"10.1145\/3371119","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":102,"title":["Interaction trees: representing recursive and impure programs in Coq"],"prefix":"10.1145","volume":"4","author":[{"given":"Li-yao","family":"Xia","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yannick","family":"Zakowski","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"He","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gregory","family":"Malecha","sequence":"additional","affiliation":[{"name":"BedRock Systems, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Interactive programming in Agda\u2013Objects and graphical user interfaces. Journal of Functional Programming 27","author":"Abel Andreas","year":"2017"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00728-4"},{"key":"e_1_2_2_4_1","volume-title":"Nils Anders Danielsson, and Nicolai Kraus","author":"Altenkirch Thorsten","year":"2017"},{"key":"e_1_2_2_5_1","volume-title":"The Operational Monad Tutorial. The Monad.Reader Issue 15","author":"Apfelmus Heinrich","year":"2010"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987212"},{"key":"e_1_2_2_7_1","volume-title":"Program Logics - for Certified Compilers","author":"Appel Andrew W."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_2_9_1","volume-title":"Ultrametric Spaces and Semantics of Programming Languages. (July","author":"Benton Nick","year":"2010"},{"key":"e_1_2_2_10_1","volume-title":"Theorem Proving in Higher Order Logics","author":"Benton Nick"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-78034-9"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-1(2:1)2005"},{"key":"e_1_2_2_13_1","volume-title":"Extensible Denotational Language Specifications. In Symposium on Theoretical Aspects of Computer Software","volume":"272","author":"Cartwright Robert","year":"1994"},{"key":"e_1_2_2_14_1","volume-title":"Technical Report. In Proceedings of the Conference on Category Theory and Computer Science.","author":"Cenciarelli Pietro","year":"1993"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_8"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_3"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250742"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","volume-title":"Certified Programming with Dependent Types","author":"Chlipala Adam","DOI":"10.7551\/mitpress\/9153.001.0001"},{"key":"e_1_2_2_20_1","volume-title":"In: International Conference on Functional Programming","author":"Danielsson Nils Anders","year":"2012"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429094"},{"key":"e_1_2_2_24_1","volume-title":"Types for Proofs and Programs, Peter Dybjer, Bengt Nordstr\u00f6m","author":"Gim\u00e9nez Eduardo"},{"key":"e_1_2_2_25_1","volume-title":"A Coinductive Calculus for Asynchronous Side-effecting Processes. CoRR abs\/1104.2936","author":"Goncharov Sergey","year":"2011"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_30"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_28_1","volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"Gu Ronghui","year":"2016"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80065-3"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_21"},{"key":"e_1_2_2_33_1","doi-asserted-by":"crossref","volume-title":"Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi","author":"Hasegawa Masahito","DOI":"10.1007\/978-1-4471-0865-8_7"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_35_1","unstructured":"Aquinas Hobor. 2008. Oracle Semantics. Ph.D. Dissertation. Princeton NJ USA. Advisor(s) Appel Andrew W. AAI3333851.  Aquinas Hobor. 2008. Oracle Semantics. Ph.D. Dissertation. Princeton NJ USA. Advisor(s) Appel Andrew W. AAI3333851."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100074338"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503791"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_45_1","volume-title":"Pierce","author":"Lampropoulos Leonidas","year":"2018"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_20"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706329"},{"key":"e_1_2_2_51_1","unstructured":"Coq development team. 2018. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.8.1.  Coq development team. 2018. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria.fr Version 8.8.1."},{"key":"e_1_2_2_52_1","unstructured":"Coq development team. 2019. The Coq proof assistant reference manual. The Gallina specification language. Co-inductive types Caveat. LogiCal Project. https:\/\/coq.inria.fr\/distrib\/V8.9.0\/refman\/language\/gallina-specification-language.html#caveat Version 8.9.0.  Coq development team. 2019. The Coq proof assistant reference manual. The Gallina specification language. Co-inductive types Caveat. LogiCal Project. https:\/\/coq.inria.fr\/distrib\/V8.9.0\/refman\/language\/gallina-specification-language.html#caveat Version 8.9.0."},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19797-5_13"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2004.05.003"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71948-7"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.32.5"},{"key":"e_1_2_2_59_1","volume-title":"Paulson","author":"Nipkow Tobias","year":"2002"},{"key":"e_1_2_2_60_1","unstructured":"Ulf Norell. 2007. Towards a practical programming language based on dependent type theory.  Ulf Norell. 2007. Towards a practical programming language based on dependent type theory."},{"key":"e_1_2_2_61_1","volume-title":"Functional Big-Step Semantics","author":"Owens Scott"},{"key":"e_1_2_2_62_1","volume-title":"Imperative Functional Programming. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: Papers Presented at the Symposium. ACM Press.","author":"Peyton Jones Simon L","year":"1993"},{"key":"e_1_2_2_63_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u02c7at\u02c7alin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2018"},{"key":"e_1_2_2_64_1","volume-title":"The Coinductive Resumption Monad. Electronic notes in theoretical computer science. 308","author":"Pir\u00f2g Maciej","year":"2014"},{"key":"e_1_2_2_65_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Plotkin Gordon"},{"key":"e_1_2_2_66_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Plotkin Gordon"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.009"},{"key":"e_1_2_2_68_1","volume-title":"A structural approach to operational semantics. J. Log. Algebr. Program. 60-61","author":"Plotkin Gordon D.","year":"2004"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_2_2_72_1","volume-title":"Object-oriented programming in dependent type theory. Trends in functional programming. 7","author":"Setzer Anton","year":"2006"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178068"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67729-3_3"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02880-3_8"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371119","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371119","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":72,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371119"],"URL":"https:\/\/doi.org\/10.1145\/3371119","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}