{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T00:48:33Z","timestamp":1772498913531,"version":"3.50.1"},"reference-count":38,"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\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","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":[[2024,1,2]]},"abstract":"<jats:p>\n            We present\n            <jats:italic toggle=\"yes\">guarded interaction trees<\/jats:italic>\n            \u2014 a structure and a fully formalized framework for representing higherorder computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present an accompanying separation logic for reasoning about guarded interaction trees. To demonstrate that guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects, we define an interpretation of a PCF-like language with effects and show that this interpretation is sound and computationally adequate; we prove the latter using a logical relation defined using the separation logic. Guarded interaction trees also allow us to combine different effects and reason about them modularly. To illustrate this point, we give a modular proof of type soundness of cross-language interactions for safe interoperability of different higher-order languages with different effects. All results in the paper are formalized in Coq using the Iris logic over guarded type theory.\n          <\/jats:p>","DOI":"10.1145\/3632854","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"332-361","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Modular Denotational Semantics for Effects with Guarded Interaction Trees"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5864-7278","authenticated-orcid":false,"given":"Dan","family":"Frumin","sequence":"first","affiliation":[{"name":"University of Groningen, Groningen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"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.1145\/3571255"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.27"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70583-3_29"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(2:6)2008"},{"key":"e_1_3_1_9_1","article-title":"Guarded Dependent Type Theory with Coinductive Types","author":"Bizjak Ales","year":"2016","unstructured":"Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers M\u00f8gelberg, and Lars Birkedal. 2016. Guarded Dependent Type Theory with Coinductive Types. CoRR abs\/1601.01586 (2016). arXiv:1601.01586 http:\/\/arxiv.org\/abs\/1601.01586.","journal-title":"CoRR"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434314"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084215"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Naohiko Hoshino. 2012. Step Indexed Realizability Semantics for a Call-by-Value Language Based on Basic Combinatorial Objects. In 2012 27th Annual IEEE Symposium on Logic in Computer Science. 385\u2013394. https:\/\/doi.org\/10.1109\/LICS.2012.74 10.1109\/LICS.2012.74.","DOI":"10.1109\/LICS.2012.74"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.29"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527324"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190215.1190220"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129518000087"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.351.13"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.020"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0052"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"e_1_3_1_31_1","unstructured":"Lucas Silver Paul He Ethan Cecchetti Andrew K Hirsch and Steve Zdancewic. 2023. Semantics for Noninterference with Interaction Trees. (2023)."},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1137\/0211062"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_11"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633358"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473578"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_24"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632854","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632854","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:10Z","timestamp":1751659450000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632854"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632854"],"URL":"https:\/\/doi.org\/10.1145\/3632854","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"}}]}}