{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:56Z","timestamp":1780994696117,"version":"3.54.1"},"reference-count":69,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"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":[[2023,8,30]]},"abstract":"<jats:p>We develop an account of dependent session protocols in concurrent separation logic for a functional language with message-passing.  \nInspired by minimalistic session calculi,  \nwe present a layered design:  \nstarting from mutable references, we build one-shot channels, session channels, and imperative channels.  \nWhereas previous work on dependent session protocols in concurrent separation logic required advanced mechanisms such as recursive domain equations and higher-order ghost state,  \nwe only require the most basic mechanisms to verify that our one-shot channels satisfy one-shot protocols,  \nand subsequently treat their specification as a black box on top of which we define dependent session protocols.  \nThis has a number of advantages in terms of simplicity, elegance, and flexibility:  \nsupport for subprotocols and guarded recursion automatically transfers from the one-shot protocols to the dependent session protocols,  \nand we easily obtain various forms of channel closing.  \nBecause the meta theory of our results is so simple,  \nwe are able to give all definitions as part of this paper,  \nand mechanize all our results using the Iris framework in less than 1000 lines of Coq.<\/jats:p>","DOI":"10.1145\/3607856","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"768-795","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6143-9031","authenticated-orcid":false,"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Semantics of Types for Mutable State. Ph. D. Dissertation","author":"Ahmed Amal","unstructured":"Amal Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. Princeton University."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-19020-1_13"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel Paul-Andr\u00e9 Melli\u00e8s Christopher D. Richards and J\u00e9r\u00f4me Vouillon. 2007. A very modal model of a modern major general type system. In POPL. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Laura Bocchi Kohei Honda Emilio Tuosto and Nobuko Yoshida. 2010. A Theory of Design-by-Contract for Distributed Multiparty Interactions. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12 10.1007\/978-3-642-15375-4_12","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Stephen D. Brookes. 2004. A Semantics for Concurrent Separation Logic. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_2 10.1007\/978-3-540-28644-8_2","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454041"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_17"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.22"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Luca Ciccone and Luca Padovani. 2020. A Dependently Typed Linear \u03c0 -Calculus in Agda. In PPDP. https:\/\/doi.org\/10.1145\/3414080.3414109 10.1145\/3414080.3414109","DOI":"10.1145\/3414080.3414109"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"The Coq Team. 2021. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.4501022 10.5281\/zenodo.4501022","DOI":"10.5281\/zenodo.4501022"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Andreea Costea Wei-Ngan Chin Shengchao Qin and Florin Craciun. 2018. Automated Modular Verification for Relaxed Communication Protocols. In APLAS. https:\/\/doi.org\/10.1007\/978-3-030-02768-1_16 10.1007\/978-3-030-02768-1_16","DOI":"10.1007\/978-3-030-02768-1_16"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Florin Craciun Tibor Kiss and Andreea Costea. 2015. Towards a Session Logic for Communication Protocols. In ICECCS. https:\/\/doi.org\/10.1109\/ICECCS.2015.33 10.1109\/ICECCS.2015.33","DOI":"10.1109\/ICECCS.2015.33"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Hoang-Hai Dang Jacques-Henri Jourdan Jan-Oliver Kaiser and Derek Dreyer. 2020. RustBelt meets relaxed memory. https:\/\/doi.org\/10.1145\/3371102 10.1145\/3371102","DOI":"10.1145\/3371102"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","unstructured":"Ornela Dardha Elena Giachino and Davide Sangiorgi. 2012. Session types revisited. In PPDP. https:\/\/doi.org\/10.1145\/2370776.2370794 10.1145\/2370776.2370794","DOI":"10.1145\/2370776.2370794"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.06.002"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Derek Dreyer Amal Ahmed and Lars Birkedal. 2011. Logical step-indexed logical relations. LMCS https:\/\/doi.org\/10.1109\/LICS.2009.34 10.1109\/LICS.2009.34","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.314.3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607859"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Matthew A. Goto Radha Jagadeesan Alan Jeffrey Corin Pitcher and James Riely. 2016. An Extensible Approach to Session Polymorphism. MSCS https:\/\/doi.org\/10.1017\/S0960129514000231 10.1017\/S0960129514000231","DOI":"10.1017\/S0960129514000231"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2022. Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. LMCS https:\/\/doi.org\/10.46298\/lmcs-18(2:16)2022 10.46298\/lmcs-18(2:16)2022","DOI":"10.46298\/lmcs-18(2:16)2022"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Dani\u00ebl Louwrink Robbert Krebbers and Jesper Bengtson. 2021. Machine-checked semantic session typing. In CPP. https:\/\/doi.org\/10.1145\/3437992.3439914 10.1145\/3437992.3439914","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR. https:\/\/doi.org\/10.1007\/3-540-57208-2_35 10.1007\/3-540-57208-2_35","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Raymond Hu Nobuko Yoshida and Kohei Honda. 2008. Session-Based Distributed Programming in Java. In ECOOP. https:\/\/doi.org\/10.1007\/978-3-540-70592-5_22 10.1007\/978-3-540-70592-5_22","DOI":"10.1007\/978-3-540-70592-5_22"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs. 2022. A Self-Dual Distillation of Session Types. In ECOOP. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.23 10.4230\/LIPIcs.ECOOP.2022.23","DOI":"10.4230\/LIPIcs.ECOOP.2022.23"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs Stephanie Balzer and Robbert Krebbers. 2022. Connectivity graphs: a method for proving deadlock freedom based on separation logic. https:\/\/doi.org\/10.1145\/3498662 10.1145\/3498662","DOI":"10.1145\/3498662"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7993904"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Thomas Bracht Laumann Jespersen Philip Munksgaard and Ken Friis Larsen. 2015. Session types for Rust. In ICFP. https:\/\/doi.org\/10.1145\/2808098.2808100 10.1145\/2808098.2808100","DOI":"10.1145\/2808098.2808100"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Jan-Oliver Kaiser Hoang-Hai Dang Derek Dreyer Ori Lahav and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2017.17 10.4230\/LIPIcs.ECOOP.2017.17","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi. 2002. Type Systems for Concurrent Programs. https:\/\/doi.org\/10.1007\/978-3-540-40007-3_26 10.1007\/978-3-540-40007-3_26","DOI":"10.1007\/978-3-540-40007-3_26"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3471874.3472979"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A General Extensible Modal Framework for Interactive Proofs in Separation Logic. https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Ralf Jung Ales Bizjak Jacques-Henri Jourdan Derek Dreyer and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26 10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976018"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","unstructured":"\u00c9tienne Lozes and Jules Villard. 2012. Shared Contract-Obedient Endpoints. In ICE. https:\/\/doi.org\/10.4204\/EPTCS.104.3 10.4204\/EPTCS.104.3","DOI":"10.4204\/EPTCS.104.3"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Glen M\u00e9vel and Jacques-Henri Jourdan. 2021. Formal verification of a concurrent bounded queue in a weak memory model. https:\/\/doi.org\/10.1145\/3473571 10.1145\/3473571","DOI":"10.1145\/3473571"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.02.002"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Dimitris Mostrous Nobuko Yoshida and Kohei Honda. 2009. Global Principal Typing in Partially Commutative Asynchronous Sessions. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_23 10.1007\/978-3-642-00590-9_23","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Nakano. 2000. A modality for recursion. In LICS. https:\/\/doi.org\/10.1109\/LICS.2000.855774 10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.016"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn. 2004. Resources Concurrency and Local Reasoning. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_4 10.1007\/978-3-540-28644-8_4","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn John C. Reynolds and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In CSL. https:\/\/doi.org\/10.1007\/3-540-44802-0_1 10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","unstructured":"Luca Padovani. 2017. A simple library implementation of binary sessions. JFP https:\/\/doi.org\/10.1017\/S0956796816000289 10.1017\/S0956796816000289","DOI":"10.1017\/S0956796816000289"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","unstructured":"Frank Pfenning and Dennis Griffith. 2015. Polarized Substructural Session Types. In FoSSaCS. https:\/\/doi.org\/10.1007\/978-3-662-46678-0_1 10.1007\/978-3-662-46678-0_1","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411290"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373818"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","unstructured":"Hannes Saffrich and Peter Thiemann. 2022. Polymorphic Typestate for Session Types. CoRR https:\/\/doi.org\/10.48550\/arXiv.2210.17335","DOI":"10.48550\/arXiv.2210.17335"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","unstructured":"Hannes Saffrich and Peter Thiemann. 2022. Relating Functional and Imperative Session Types. LMCS https:\/\/doi.org\/10.46298\/lmcs-18(3:33)2022 10.46298\/lmcs-18(3:33)2022","DOI":"10.46298\/lmcs-18(3:33)2022"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In ECOOP. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2016.21 10.4230\/LIPIcs.ECOOP.2016.21","DOI":"10.4230\/LIPIcs.ECOOP.2016.21"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","unstructured":"Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited. POPL https:\/\/doi.org\/10.1145\/3290343 10.1145\/3290343","DOI":"10.1145\/3290343"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9 10.1007\/978-3-642-54833-8_9","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","unstructured":"Joseph Tassarotti Ralf Jung and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_34 10.1007\/978-3-662-54434-1_34","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","unstructured":"Peter Thiemann. 2019. Intrinsically-Typed Mechanized Semantics for Session Types. In PPDP. https:\/\/doi.org\/10.1145\/3354166.3354184 10.1145\/3354166.3354184","DOI":"10.1145\/3354166.3354184"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371135"},{"key":"e_1_2_1_64_1","volume-title":"A Logical Foundation for Session-Based Concurrent Computation. Ph. D. Dissertation","author":"Toninho Bernardo","unstructured":"Bernardo Toninho. 2015. A Logical Foundation for Session-Based Concurrent Computation. Ph. D. Dissertation. Carnegie Mellon University and New University of Lisbon."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho Lu\u00eds Caires and Frank Pfenning. 2011. Dependent session types via intuitionistic linear type theory. In PPDP. https:\/\/doi.org\/10.1145\/2003476.2003499 10.1145\/2003476.2003499","DOI":"10.1145\/2003476.2003499"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho Lu\u00eds Caires and Frank Pfenning. 2013. Higher-Order Processes Functions and Sessions: A Monadic Integration. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_20 10.1007\/978-3-642-37036-6_20","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho and Nobuko Yoshida. 2018. Depending on Session-Typed Processes. In FOSSACS. https:\/\/doi.org\/10.1007\/978-3-319-89366-2_7 10.1007\/978-3-319-89366-2_7","DOI":"10.1007\/978-3-319-89366-2_7"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","unstructured":"Philip Wadler. 2012. Propositions as Sessions. In ICFP. https:\/\/doi.org\/10.1145\/2364527.2364568 10.1145\/2364527.2364568","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","unstructured":"Fangyi Zhou Francisco Ferreira Raymond Hu Rumyana Neykova and Nobuko Yoshida. 2020. Statically verified refinements for multiparty protocols. https:\/\/doi.org\/10.1145\/3428216 10.1145\/3428216","DOI":"10.1145\/3428216"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607856","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607856","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:06Z","timestamp":1750178226000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607856"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":69,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607856"],"URL":"https:\/\/doi.org\/10.1145\/3607856","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}