{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T04:14:40Z","timestamp":1746591280902,"version":"3.40.5"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031911200"},{"type":"electronic","value":"9783031911217"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Guarded Interaction Trees are a structure and a fully formalized framework\u00a0for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That is, effects whose behaviors depend on the evaluation context, e.g., ,  and . Using and reasoning about such effects is challenging since certain compositionality principles no longer hold in the presence of such effects. For example, the so-called \u201cbind rule\u201d in modern program logics (which allows one to reason modularly about a term inside a context) is no longer valid. The goal of our extension is to support representation and reasoning about context-dependent effects in the most painless way possible. To that end, our extension is conservative: the reasoning principles (and the Coq implementation) for context-independent effects remain the same. We show that our implementation of context-dependent effects is viable and powerful. We use it to give direct-style denotational semantics for higher-order programming languages with  and with delimited continuations. We extend the program logic for Guarded Interaction Trees to account for context-dependent effects, and we use the program logic to prove that\u00a0the denotational semantics is adequate with respect to the operational semantics. This is achieved by constructing logical relations between syntax and semantics inside the program logic. Additionally, we retain the ability to combine multiple effects in a modular way, which we demonstrate by showing type soundness for safe interoperability of a programming language with delimited continuations and a programming language with higher-order store.<\/jats:p>","DOI":"10.1007\/978-3-031-91121-7_12","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T11:51:08Z","timestamp":1746186668000},"page":"286-313","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Context-Dependent Effects in Guarded Interaction Trees"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7322-5644","authenticated-orcid":false,"given":"Sergei","family":"Stepanenko","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emma","family":"Nardino","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5864-7278","authenticated-orcid":false,"given":"Dan","family":"Frumin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"12_CR1","unstructured":"Asai, K.: Logical relations for call-by-value delimited continuations. In: van Eekelen, M.C.J.D. (ed.) Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005. Trends in Functional Programming, vol.\u00a06, pp. 63\u201378. Intellect (2005)"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Asai, K., Kameyama, Y.: Polymorphic Delimited Continuations. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 239\u2013254. Springer. https:\/\/doi.org\/10.1007\/978-3-540-76637-7_16","DOI":"10.1007\/978-3-540-76637-7_16"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Bach\u00a0Poulsen, C., van der Rest, C.: Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects. Proceedings of the ACM on Programming Languages 7(POPL), 62:1801\u201362:1831 (Jan 2023). https:\/\/doi.org\/10.1145\/3571255","DOI":"10.1145\/3571255"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming 84(1), 108\u2013123 (Jan 2015). https:\/\/doi.org\/10.1016\/j.jlamp.2014.02.001","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Biernacka, M., Biernacki, D.: Context-based proofs of termination for typed delimited-control operators. In: Porto, A., L\u00f3pez-Fraguas, F.J. (eds.) Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal. pp. 289\u2013300. ACM (2009). https:\/\/doi.org\/10.1145\/1599410.1599446, https:\/\/doi.org\/10.1145\/1599410.1599446","DOI":"10.1145\/1599410.1599446"},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Biernacka, M., Biernacki, D., Danvy, O.: An operational foundation for delimited continuations in the CPS hierarchy. Log. Methods Comput. Sci. 1(2) (2005). https:\/\/doi.org\/10.2168\/LMCS-1(2:5)2005, https:\/\/doi.org\/10.2168\/LMCS-1(2:5)2005","DOI":"10.2168\/LMCS-1(2:5)2005"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Biernacki, D., Pir\u00f3g, M., Polesiuk, P., Sieczkowski, F.: Abstracting algebraic effects. Proc. ACM Program. Lang. 3(POPL) (jan 2019). https:\/\/doi.org\/10.1145\/3290319, https:\/\/doi.org\/10.1145\/3290319","DOI":"10.1145\/3290319"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Birkedal, L., M\u00f8gelberg, R.E., Schwinghammer, J., St\u00f8vring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci. 8(4) (2012). https:\/\/doi.org\/10.2168\/LMCS-8(4:1)2012, https:\/\/doi.org\/10.2168\/LMCS-8(4:1)2012","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Cartwright, R., Felleisen, M.: Extensible denotational language specifications. In: Hagiya, M., Mitchell, J.C. (eds.) Theoretical Aspects of Computer Software. pp. 244\u2013272. Springer, Berlin, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57887-0_99","DOI":"10.1007\/3-540-57887-0_99"},{"key":"12_CR10","unstructured":"Danvy, O., Filinski, A.: A functional abstraction of typed contexts. Tech. rep., DIKU \u2013 Computer Science Department, University of Copenhagen (1989)"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Dyvbig, R.K., Peyton\u00a0Jones, S., Sabry, A.: A monadic framework for delimited continuations 17(6), 687\u2013730. https:\/\/doi.org\/10.1017\/S0956796807006259, https:\/\/www.cambridge.org\/core\/journals\/journal-of-functional-programming\/article\/monadic-framework-for-delimited-continuations\/D99D1394370DFA8EA8428D552B5D8E7E","DOI":"10.1017\/S0956796807006259"},{"key":"12_CR12","unstructured":"Felleisen, M., Friedman, D.P.: Control operators, the secd-machine, and the $$\\lambda $$-calculus. In: Wirsing, M. (ed.) Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986. pp. 193\u2013222. North-Holland (1987)"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Frumin, D., Timany, A., Birkedal, L.: Modular denotational semantics for effects with guarded interaction trees. Proc. ACM Program. Lang. 8(POPL), 332\u2013361 (2024). https:\/\/doi.org\/10.1145\/3632854, https:\/\/doi.org\/10.1145\/3632854","DOI":"10.1145\/3632854"},{"key":"12_CR14","unstructured":"Iris team: The Iris Project website and Coq development (2025), https:\/\/iris-project.org\/"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, \u00a0e20 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151, https:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"12_CR16","unstructured":"King, A.: Delimited continuation primops. https:\/\/github.com\/ghc-proposals\/ghc-proposals\/blob\/master\/proposals\/0313-delimited-continuation-primops.rst (2021), accessed: 2024-06-27"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Kiselyov, O., Shan, C.c.: A Substructural Type System for Delimited Continuations. In: Della\u00a0Rocca, S.R. (ed.) Typed Lambda Calculi and Applications. pp. 223\u2013239. Springer, Berlin, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73228-0_17","DOI":"10.1007\/978-3-540-73228-0_17"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Koh, N., Li, Y., Li, Y., Xia, L.y., Beringer, L., Honor\u00e9, W., Mansky, W., Pierce, B.C., Zdancewic, S.: From C to interaction trees: Specifying, verifying, and testing a networked server. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 234\u2013248. CPP 2019, Association for Computing Machinery, New York, NY, USA (Jan 201). https:\/\/doi.org\/10.1145\/3293880.3294106","DOI":"10.1145\/3293880.3294106"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 205\u2013217. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009855, https:\/\/doi.org\/10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Leijen, D.: Koka: Programming with row polymorphic effect types. In: Levy, P.B., Krishnaswami, N. (eds.) Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2014, Grenoble, France, 12 April 2014. EPTCS, vol.\u00a0153, pp. 100\u2013126 (2014). https:\/\/doi.org\/10.4204\/EPTCS.153.8, https:\/\/doi.org\/10.4204\/EPTCS.153.8","DOI":"10.4204\/EPTCS.153.8"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Leijen, D.: Structured asynchrony with algebraic effects. In: Lindley, S., Yorgey, B.A. (eds.) Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2017, Oxford, UK, September 3, 2017. pp. 16\u201329. ACM (2017). https:\/\/doi.org\/10.1145\/3122975.3122977, https:\/\/doi.org\/10.1145\/3122975.3122977","DOI":"10.1145\/3122975.3122977"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Materzok, M., Biernacki, D.: Subtyping delimited continuations 46(9), 81\u20139. https:\/\/doi.org\/10.1145\/2034574.2034786, https:\/\/doi.org\/10.1145\/2034574.2034786","DOI":"10.1145\/2034574.2034786"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Typed operational reasoning. In: Pierce, B.C. (ed.) Advanced Topics In Types And Programming Languages, chap.\u00a07, pp. 245\u2013289. The MIT Press (2004)","DOI":"10.7551\/mitpress\/1104.003.0011"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D., Pretnar, M.: Handling Algebraic Effects. Logical Methods in Computer Science Volume 9, Issue 4 (Dec 2013). https:\/\/doi.org\/10.2168\/LMCS-9(4:23)2013","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"12_CR25","unstructured":"Silver, L., He, P., Cecchetti, E., Hirsch, A.K., Zdancewic, S.: Semantics for Noninterference with Interaction Trees (2023)"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Sitaram, D., Felleisen, M.: Models of continuations without continuations. In: Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 185\u2013196. POPL \u201991, Association for Computing Machiner. https:\/\/doi.org\/10.1145\/99583.99611, https:\/\/dl.acm.org\/doi\/10.1145\/99583.99611","DOI":"10.1145\/99583.99611"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Stepanenko, S., Nardino, E., Frumin, D., Timany, A., Birkedal, L.: Context-dependent effects in guarded interaction trees (Jan 2025). https:\/\/doi.org\/10.5281\/zenodo.14623650, https:\/\/doi.org\/10.5281\/zenodo.14623650","DOI":"10.5281\/zenodo.14623650"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Timany, A., Birkedal, L.: Mechanized relational verification of concurrent programs with continuations. Proc. ACM Program. Lang. 3(ICFP), 105:1\u2013105:28 (2019). https:\/\/doi.org\/10.1145\/3341709, https:\/\/doi.org\/10.1145\/3341709","DOI":"10.1145\/3341709"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Timany, A., Gu\u00e9neau, A., Birkedal, L.: The logical essence of well-bracketed control flow. Proc. ACM Program. Lang. 8(POPL), 575\u2013603 (2024). https:\/\/doi.org\/10.1145\/3632862, https:\/\/doi.org\/10.1145\/3632862","DOI":"10.1145\/3632862"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Timany, A., Krebbers, R., Dreyer, D., Birkedal, L.: A logical approach to type soundness. Journal of the ACM 71 (2024)","DOI":"10.1145\/3676954"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"van den Berg, B., Schrijvers, T., Poulsen, C.B., Wu, N.: Latent Effects for Reusable Language Components. In: Oh, H. (ed.) Programming Languages and Systems. pp. 182\u2013201. Lecture Notes in Computer Science, Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89051-3_11","DOI":"10.1007\/978-3-030-89051-3_11"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"de\u00a0Vilhena, P.E., Pottier, F.: A separation logic for effect handlers. Proc. ACM Program. Lang. 5(POPL) (jan 2021). https:\/\/doi.org\/10.1145\/3434314, https:\/\/doi.org\/10.1145\/3434314","DOI":"10.1145\/3434314"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Wu, N., Schrijvers, T., Hinze, R.: Effect handlers in scope. In: Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell. pp. 1\u201312. Haskell \u201914, Association for Computing Machinery, New York, NY, USA (Sep 2014). https:\/\/doi.org\/10.1145\/2633357.2633358","DOI":"10.1145\/2633357.2633358"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Xia, L., Zakowski, Y., He, P., Hur, C., Malecha, G., Pierce, B.C., Zdancewic, S.: Interaction trees: representing recursive and impure programs in coq. Proc. ACM Program. Lang. 4(POPL), 51:1\u201351:32 (2020). https:\/\/doi.org\/10.1145\/3371119, https:\/\/doi.org\/10.1145\/3371119","DOI":"10.1145\/3371119"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"Zakowski, Y., Beck, C., Yoon, I., Zaichuk, I., Zaliva, V., Zdancewic, S.: Modular, compositional, and executable formal semantics for LLVM IR. Proceedings of the ACM on Programming Languages 5(ICFP), 67:1\u201367:30 (Aug 2021). https:\/\/doi.org\/10.1145\/3473572","DOI":"10.1145\/3473572"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Zhang, H., Honor\u00e9, W., Koh, N., Li, Y., Li, Y., Xia, L.Y., Beringer, L., Mansky, W., Pierce, B., Zdancewic, S.: Verifying an HTTP Key-Value Server with Interaction Trees and VST. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0193, pp. 32:1\u201332:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.32","DOI":"10.4230\/LIPIcs.ITP.2021.32"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-91121-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T08:38:28Z","timestamp":1746520708000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-91121-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031911200","9783031911217"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-91121-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The formalisation associated with this paper, which covers all the main results, is available online\u00a0[].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data-Availability Statement"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}