{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:42:31Z","timestamp":1754487751878,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"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,1,9]]},"abstract":"<jats:p>We present a Separation Logic with space credits for reasoning about heap space in a sequential call-by-value lambda-calculus equipped with garbage collection and mutable state. A key challenge is to design sound, modular, lightweight mechanisms for establishing the unreachability of a block. Prior work in this area uses pointed-by assertions to keep track of the predecessors of every block, but is carried out in the setting of an assembly-like programming language. We take up the challenge in the setting of a high-level language, where a key problem is to identify and reason about the memory locations that the garbage collector considers as roots. For this purpose, we propose novel \"stackable\" assertions, which keep track of the existence of stack-to-heap pointers without explicitly recording their origin. Furthermore, we explain how to reason about closures -- concrete heap-allocated data structures that implement the abstract concept of a first-class function. We demonstrate the expressiveness and tractability of our program logic via a range of examples, including recursive functions on linked lists, objects implemented using closures and mutable internal state, recursive functions in continuation-passing style, and three stack implementations that exhibit different space bounds. These last three examples illustrate reasoning about the reachability of the items stored in a container as well as amortized reasoning about space. All of our results are proved in Coq on top of Iris.<\/jats:p>","DOI":"10.1145\/3571218","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"718-747","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A High-Level Separation Logic for Heap Space under Garbage Collection"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2169-1977","authenticated-orcid":false,"given":"Alexandre","family":"Moine","sequence":"first","affiliation":[{"name":"Inria, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7764-4507","authenticated-orcid":false,"given":"Arthur","family":"Chargu\u00e9raud","sequence":"additional","affiliation":[{"name":"Inria, France \/ Universit\u00e9 de Strasbourg, France \/ CNRS, France \/ ICube, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, France"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12466-7_1"},{"volume-title":"Compiling with Continuations","author":"Appel Andrew W.","key":"e_1_2_1_2_1","unstructured":"Andrew W. Appel . 1992. Compiling with Continuations . Cambridge University Press . http:\/\/www.cambridge.org\/9780521033114 Andrew W. Appel. 1992. Compiling with Continuations. Cambridge University Press. http:\/\/www.cambridge.org\/9780521033114"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.003"},{"key":"e_1_2_1_4_1","volume-title":"Another Type System for In-Place Update. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"52","author":"Aspinall David","year":"2002","unstructured":"David Aspinall and Martin Hofmann . 2002 . Another Type System for In-Place Update. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science , Vol. 2305). Springer, 36\u2013 52 . https:\/\/www.tcs.ifi.lmu.de\/mitarbeiter\/martin-hofmann\/publikationen-pdfs\/c22-anothertypesystem.pdf David Aspinall and Martin Hofmann. 2002. Another Type System for In-Place Update. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 2305). Springer, 36\u201352. https:\/\/www.tcs.ifi.lmu.de\/mitarbeiter\/martin-hofmann\/publikationen-pdfs\/c22-anothertypesystem.pdf"},{"key":"e_1_2_1_5_1","volume-title":"Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science, 7, 2:17","author":"Atkey Robert","year":"2011","unstructured":"Robert Atkey . 2011. Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science, 7, 2:17 ( 2011 ), http:\/\/bentnib.org\/amortised-sep-logic-journal.pdf Robert Atkey. 2011. Amortised Resource Analysis with Separation Logic. Logical Methods in Computer Science, 7, 2:17 (2011), http:\/\/bentnib.org\/amortised-sep-logic-journal.pdf"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9496-y"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093635499"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Richard Bornat Cristiano Calcagno Peter O\u2019Hearn and Matthew Parkinson. 2005. Permission accounting in separation logic. In Principles of Programming Languages (POPL). 259\u2013270. http:\/\/www.cs.ucl.ac.uk\/staff\/p.ohearn\/papers\/permissions_paper.pdf Richard Bornat Cristiano Calcagno Peter O\u2019Hearn and Matthew Parkinson. 2005. Permission accounting in separation logic. In Principles of Programming Languages (POPL). 259\u2013270. http:\/\/www.cs.ucl.ac.uk\/staff\/p.ohearn\/papers\/permissions_paper.pdf","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_1_9_1","volume-title":"Checking Interference with Fractional Permissions. In Static Analysis Symposium (SAS) (Lecture Notes in Computer Science","volume":"72","author":"Boyland John","year":"2003","unstructured":"John Boyland . 2003 . Checking Interference with Fractional Permissions. In Static Analysis Symposium (SAS) (Lecture Notes in Computer Science , Vol. 2694). Springer, 55\u2013 72 . http:\/\/www.cs.uwm.edu\/~boyland\/papers\/permissions.pdf John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis Symposium (SAS) (Lecture Notes in Computer Science, Vol. 2694). Springer, 55\u201372. http:\/\/www.cs.uwm.edu\/~boyland\/papers\/permissions.pdf"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Quentin Carbonneaux Jan Hoffmann Tahina Ramananandro and Zhong Shao. 2014. End-to-end verification of stack-space bounds for C programs. In Programming Language Design and Implementation (PLDI). 270\u2013281. http:\/\/flint.cs.yale.edu\/flint\/publications\/veristack.pdf Quentin Carbonneaux Jan Hoffmann Tahina Ramananandro and Zhong Shao. 2014. End-to-end verification of stack-space bounds for C programs. In Programming Language Design and Implementation (PLDI). 270\u2013281. http:\/\/flint.cs.yale.edu\/flint\/publications\/veristack.pdf","DOI":"10.1145\/2666356.2594301"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Quentin Carbonneaux Jan Hoffmann and Zhong Shao. 2015. Compositional certified resource bounds. In Programming Language Design and Implementation (PLDI). 467\u2013478. https:\/\/www.cs.yale.edu\/homes\/hoffmann\/papers\/amort_imp15.pdf Quentin Carbonneaux Jan Hoffmann and Zhong Shao. 2015. Compositional certified resource bounds. In Programming Language Design and Implementation (PLDI). 467\u2013478. https:\/\/www.cs.yale.edu\/homes\/hoffmann\/papers\/amort_imp15.pdf","DOI":"10.1145\/2813885.2737955"},{"key":"e_1_2_1_13_1","article-title":"Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits","author":"Chargu\u00e9raud Arthur","year":"2017","unstructured":"Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier . 2017 . Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits . Journal of Automated Reasoning , Sept. , http:\/\/cambium.inria.fr\/~fpottier\/publis\/chargueraud-pottier-uf-sltc.pdf Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2017. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. Journal of Automated Reasoning, Sept., http:\/\/cambium.inria.fr\/~fpottier\/publis\/chargueraud-pottier-uf-sltc.pdf","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375656"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_7"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_2_1_17_1","unstructured":"William R. Cook. 2009. On understanding data abstraction revisited. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). 557\u2013572. http:\/\/www.cs.utexas.edu\/~wcook\/Drafts\/2009\/essay.pdf William R. Cook. 2009. On understanding data abstraction revisited. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). 557\u2013572. http:\/\/www.cs.utexas.edu\/~wcook\/Drafts\/2009\/essay.pdf"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Karl Crary and Stephanie Weirich. 2000. Resource bound certification. In Principles of Programming Languages (POPL). 184\u2013198. http:\/\/www.cs.cornell.edu\/talc\/papers\/resource_bound\/res.pdf Karl Crary and Stephanie Weirich. 2000. Resource bound certification. In Principles of Programming Languages (POPL). 184\u2013198. http:\/\/www.cs.cornell.edu\/talc\/papers\/resource_bound\/res.pdf","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0211-0"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428272"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70247-7"},{"key":"e_1_2_1_23_1","volume-title":"Hallet and Assaf Kfoury","author":"Joseph","year":"2005","unstructured":"Joseph J. Hallet and Assaf Kfoury . 2005 . A Formal Semantics for Weak References. Boston University . https:\/\/open.bu.edu\/handle\/2144\/1857 Joseph J. Hallet and Assaf Kfoury. 2005. A Formal Semantics for Weak References. Boston University. https:\/\/open.bu.edu\/handle\/2144\/1857"},{"key":"e_1_2_1_24_1","volume-title":"European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"319","author":"Maximilian P.","unstructured":"Maximilian P. L. Haslbeck and Peter Lammich. 2021. For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM . In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science , Vol. 12648). Springer, 292\u2013 319 . https:\/\/www21.in.tum.de\/~haslbema\/documents\/Haslbeck_Lammich_LLVM_with_Time.pdf Maximilian P. L. Haslbeck and Peter Lammich. 2021. For a Few Dollars More - Verified Fine-Grained Algorithm Analysis Down to LLVM. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 12648). Springer, 292\u2013319. https:\/\/www21.in.tum.de\/~haslbema\/documents\/Haslbeck_Lammich_LLVM_with_Time.pdf"},{"key":"e_1_2_1_25_1","volume-title":"Haslbeck and Tobias Nipkow","author":"Maximilian P.","year":"2018","unstructured":"Maximilian P. L. Haslbeck and Tobias Nipkow . 2018 . Hoare Logics for Time Bounds: A Study in Meta Theory. In Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science , Vol. 10805). Springer, 155\u2013 171 . https:\/\/www21.in.tum.de\/~nipkow\/pubs\/tacas18.pdf Maximilian P. L. Haslbeck and Tobias Nipkow. 2018. Hoare Logics for Time Bounds: A Study in Meta Theory. In Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 10805). Springer, 155\u2013171. https:\/\/www21.in.tum.de\/~nipkow\/pubs\/tacas18.pdf"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/263698.263733"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_14"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In Principles of Programming Languages (POPL). 359\u2013373. http:\/\/www.cs.cmu.edu\/~janh\/papers\/HoffmannDW17.pdf Jan Hoffmann Ankush Das and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In Principles of Programming Languages (POPL). 359\u2013373. http:\/\/www.cs.cmu.edu\/~janh\/papers\/HoffmannDW17.pdf","DOI":"10.1145\/3093333.3009842"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782641"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/763845.763847"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Steffen Jost. 2003. Static prediction of heap space usage for first-order functional programs. In Principles of Programming Languages (POPL). 185\u2013197. http:\/\/www2.tcs.ifi.lmu.de\/~jost\/research\/POPL_2003_Jost_Hofmann.pdf Martin Hofmann and Steffen Jost. 2003. Static prediction of heap space usage for first-order functional programs. In Principles of Programming Languages (POPL). 185\u2013197. http:\/\/www2.tcs.ifi.lmu.de\/~jost\/research\/POPL_2003_Jost_Hofmann.pdf","DOI":"10.1145\/640128.604148"},{"key":"e_1_2_1_35_1","volume-title":"Type-Based Amortised Heap-Space Analysis. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science","volume":"37","author":"Hofmann Martin","year":"2006","unstructured":"Martin Hofmann and Steffen Jost . 2006 . Type-Based Amortised Heap-Space Analysis. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science , Vol. 3924). Springer, 22\u2013 37 . https:\/\/www.tcs.ifi.lmu.de\/mitarbeiter\/martin-hofmann\/publikationen-pdfs\/c36-typebasedamortisedheap-space.pdf Martin Hofmann and Steffen Jost. 2006. Type-Based Amortised Heap-Space Analysis. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science, Vol. 3924). Springer, 22\u201337. https:\/\/www.tcs.ifi.lmu.de\/mitarbeiter\/martin-hofmann\/publikationen-pdfs\/c36-typebasedamortisedheap-space.pdf"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_24"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_32"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Chung-Kil Hur Derek Dreyer and Viktor Vafeiadis. 2011. Separation Logic in the Presence of Garbage Collection. In Logic in Computer Science (LICS). 247\u2013256. http:\/\/people.mpi-sws.org\/~dreyer\/papers\/gcsl\/paper.pdf Chung-Kil Hur Derek Dreyer and Viktor Vafeiadis. 2011. Separation Logic in the Presence of Garbage Collection. In Logic in Computer Science (LICS). 247\u2013256. http:\/\/people.mpi-sws.org\/~dreyer\/papers\/gcsl\/paper.pdf","DOI":"10.1109\/LICS.2011.46"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_10"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_2_1_42_1","unstructured":"Xavier Leroy. 2021. The CompCert C compiler. http:\/\/compcert.org\/ Xavier Leroy. 2021. The CompCert C compiler. http:\/\/compcert.org\/"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(92)90011-9"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the ACM on Programming Languages, 6, POPL (2022","author":"Madiot Jean-Marie","year":"2022","unstructured":"Jean-Marie Madiot and Fran\u00e7ois Pottier . 2022 . A Separation Logic for Heap Space under Garbage Collection . Proceedings of the ACM on Programming Languages, 6, POPL (2022 ), Jan., http:\/\/cambium.inria.fr\/~fpottier\/publis\/madiot-pottier-diamonds- 2022.pdf Jean-Marie Madiot and Fran\u00e7ois Pottier. 2022. A Separation Logic for Heap Space under Garbage Collection. Proceedings of the ACM on Programming Languages, 6, POPL (2022), Jan., http:\/\/cambium.inria.fr\/~fpottier\/publis\/madiot-pottier-diamonds-2022.pdf"},{"key":"e_1_2_1_45_1","doi-asserted-by":"crossref","unstructured":"Alexandre Moine Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2022. A High-Level Separation Logic for Heap Space under Garbage Collection (Extended Version). https:\/\/hal.inria.fr\/hal-03823056 Alexandre Moine Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2022. A High-Level Separation Logic for Heap Space under Garbage Collection (Extended Version). https:\/\/hal.inria.fr\/hal-03823056","DOI":"10.1145\/3571218"},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Alexandre Moine Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2022. A High-Level Separation Logic for Heap Space under Garbage Collection (Proof Artifact). https:\/\/gitlab.inria.fr\/amoine\/spacelambda Alexandre Moine Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2022. A High-Level Separation Logic for Heap Space under Garbage Collection (Proof Artifact). https:\/\/gitlab.inria.fr\/amoine\/spacelambda","DOI":"10.1145\/3571218"},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"J. Gregory Morrisett Matthias Felleisen and Robert Harper. 1995. Abstract Models of Memory Management. In Functional Programming Languages and Computer Architecture (FPCA). 66\u201377. https:\/\/www.cs.cmu.edu\/~rwh\/papers\/gc\/fpca95.pdf J. Gregory Morrisett Matthias Felleisen and Robert Harper. 1995. Abstract Models of Memory Management. In Functional Programming Languages and Computer Architecture (FPCA). 66\u201377. https:\/\/www.cs.cmu.edu\/~rwh\/papers\/gc\/fpca95.pdf","DOI":"10.1145\/224164.224182"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_2_1_50_1","volume-title":"Logic for Programming Artificial Intelligence and Reasoning (LPAR) (EPiC Series in Computing","volume":"563","author":"Niu Yue","year":"2018","unstructured":"Yue Niu and Jan Hoffmann . 2018 . Automatic Space Bound Analysis for Functional Programs with Garbage Collection . In Logic for Programming Artificial Intelligence and Reasoning (LPAR) (EPiC Series in Computing , Vol. 57). 543\u2013 563 . https:\/\/easychair.org\/publications\/paper\/dcnD Yue Niu and Jan Hoffmann. 2018. Automatic Space Bound Analysis for Functional Programs with Garbage Collection. In Logic for Programming Artificial Intelligence and Reasoning (LPAR) (EPiC Series in Computing, Vol. 57). 543\u2013563. https:\/\/easychair.org\/publications\/paper\/dcnD"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341687"},{"volume-title":"User-defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction","author":"Reynolds John C.","key":"e_1_2_1_53_1","unstructured":"John C. Reynolds . 1975. User-defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction . Carnegie Mellon University . http:\/\/repository.cmu.edu\/compsci\/1278\/ John C. Reynolds. 1975. User-defined Types and Procedural Data Structures as Complementary Approaches to Data Abstraction. Carnegie Mellon University. http:\/\/repository.cmu.edu\/compsci\/1278\/"},{"key":"e_1_2_1_54_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS). 55\u201374","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds . 2002 . Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS). 55\u201374 . http:\/\/www.cs.cmu.edu\/~jcr\/seplogic.pdf John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS). 55\u201374. http:\/\/www.cs.cmu.edu\/~jcr\/seplogic.pdf"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968168"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571218","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571218","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571218"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571218"],"URL":"https:\/\/doi.org\/10.1145\/3571218","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}