{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T19:37:51Z","timestamp":1790451471176,"version":"4.1.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"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":[[2022,1,16]]},"abstract":"<jats:p>We present SL\u2662, a Separation Logic that allows controlling the heap space consumption of a program in the presence of dynamic memory allocation and garbage collection. A user of the logic works with space credits, a resource that is consumed when an object is allocated and produced when a group of objects is logically deallocated, that is, when the user is able to prove that it has become unreachable and therefore can be collected. To prove such a fact, the user maintains pointed-by assertions that record the immediate predecessors of every object. Our calculus, SpaceLang, has mutable state, shared-memory concurrency, and code pointers. We prove that SL\u2662 is sound and present several simple examples of its use.<\/jats:p>","DOI":"10.1145\/3498672","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T12:03:12Z","timestamp":1641988992000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A separation logic for heap space under garbage collection"],"prefix":"10.1145","volume":"6","author":[{"given":"Jean-Marie","family":"Madiot","sequence":"first","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4069-1235","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Pottier","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1296907.1296922"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542431.1542450"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806651.1806671"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.10.008"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.003"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021014.79255.33"},{"key":"e_1_2_2_7_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_2_8_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_2_9_1","volume-title":"International Conference on Functional Programming (ICFP). 213\u2013225","author":"Guy","unstructured":"Guy E. Blelloch and John Greiner. 1996. A Provable Time and Space Efficient Implementation of NESL . In International Conference on Functional Programming (ICFP). 213\u2013225 . http:\/\/www.cs.cmu.edu\/~guyb\/papers\/BG96nesl.pdf Guy E. Blelloch and John Greiner. 1996. A Provable Time and Space Efficient Implementation of NESL. In International Conference on Functional Programming (ICFP). 213\u2013225. http:\/\/www.cs.cmu.edu\/~guyb\/papers\/BG96nesl.pdf"},{"key":"e_1_2_2_10_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_2_11_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_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375655"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2006.5.5.a2"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_2_15_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_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408998"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/362790.362798"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375634.1375656"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_7"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/367487.367501"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.1656"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428272"},{"key":"e_1_2_2_24_1","volume-title":"Automated Verification of Practical Garbage Collectors. Logical Methods in Computer Science, 6, 3","author":"Hawblitzel Chris","year":"2010","unstructured":"Chris Hawblitzel and Erez Petrank . 2010. Automated Verification of Practical Garbage Collectors. Logical Methods in Computer Science, 6, 3 ( 2010 ), arxiv:1004.3808 Chris Hawblitzel and Erez Petrank. 2010. Automated Verification of Practical Garbage Collectors. Logical Methods in Computer Science, 6, 3 (2010), arxiv:1004.3808"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_14"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_2_28_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_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782641"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/763845.763847"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"e_1_2_2_32_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_2_33_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_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_24"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_32"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317785"},{"key":"e_1_2_2_37_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_2_38_1","unstructured":"Iris. 2021. iris.base_logic.lib.gen_heap. https:\/\/plv.mpi-sws.org\/coqdoc\/iris\/iris.base_logic.lib.gen_heap.html Iris. 2021. iris.base_logic.lib.gen_heap. https:\/\/plv.mpi-sws.org\/coqdoc\/iris\/iris.base_logic.lib.gen_heap.html"},{"key":"e_1_2_2_39_1","doi-asserted-by":"crossref","unstructured":"Steffen Jost Kevin Hammond Hans-Wolfgang Loidl and Martin Hofmann. 2010. Static determination of quantitative resource usage for higher-order programs. In Principles of Programming Languages (POPL). 223\u2013236. http:\/\/www2.tcs.ifi.lmu.de\/~jost\/research\/POPL_2010__Higher-Order_AA__Jost_etAl.pdf Steffen Jost Kevin Hammond Hans-Wolfgang Loidl and Martin Hofmann. 2010. Static determination of quantitative resource usage for higher-order programs. In Principles of Programming Languages (POPL). 223\u2013236. http:\/\/www2.tcs.ifi.lmu.de\/~jost\/research\/POPL_2010__Higher-Order_AA__Jost_etAl.pdf","DOI":"10.1145\/1707801.1706327"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_23"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9398-9"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473581"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_10"},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","unstructured":"Jean-Marie Madiot and Fran\u00e7ois Pottier. 2021. A Separation Logic for Heap Space under Garbage Collection (Repository). https:\/\/gitlab.inria.fr\/fpottier\/diamonds Jean-Marie Madiot and Fran\u00e7ois Pottier. 2021. A Separation Logic for Heap Space under Garbage Collection (Repository). https:\/\/gitlab.inria.fr\/fpottier\/diamonds","DOI":"10.1145\/3498672"},{"key":"e_1_2_2_46_1","volume-title":"International Conference on Functional Programming (ICFP). 273\u2013284","author":"McCreight Andrew","unstructured":"Andrew McCreight , Tim Chevalier , and Andrew P. Tolmach . 2010. A certified framework for compiling and executing garbage-collected languages . In International Conference on Functional Programming (ICFP). 273\u2013284 . https:\/\/web.cecs.pdx.edu\/~apt\/icfp10.pdf Andrew McCreight, Tim Chevalier, and Andrew P. Tolmach. 2010. A certified framework for compiling and executing garbage-collected languages. In International Conference on Functional Programming (ICFP). 273\u2013284. https:\/\/web.cecs.pdx.edu\/~apt\/icfp10.pdf"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250788"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80286-5"},{"key":"e_1_2_2_49_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_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"e_1_2_2_51_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_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_2_2_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_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9487-z"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364575"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796810000146"},{"key":"e_1_2_2_58_1","doi-asserted-by":"crossref","unstructured":"Mads Tofte and Jean-Pierre Talpin. 1994. Implementation of the Typed Call-by-Value \u03bb -Calculus using a Stack of Regions. In Principles of Programming Languages (POPL). 188\u2013201. http:\/\/www.irisa.fr\/prive\/talpin\/papers\/popl94.pdf Mads Tofte and Jean-Pierre Talpin. 1994. Implementation of the Typed Call-by-Value \u03bb -Calculus using a Stack of Regions. In Principles of Programming Languages (POPL). 188\u2013201. http:\/\/www.irisa.fr\/prive\/talpin\/papers\/popl94.pdf","DOI":"10.1145\/174675.177855"},{"key":"e_1_2_2_59_1","volume-title":"International Symposium on Memory Management. 139\u2013148","author":"Unnikrishnan Leena","year":"2009","unstructured":"Leena Unnikrishnan and Scott D. Stoller . 2009. Parametric heap usage analysis for functional programs . In International Symposium on Memory Management. 139\u2013148 . https:\/\/www3.cs.stonybrook.edu\/~stoller\/papers\/ismm 2009 .pdf Leena Unnikrishnan and Scott D. Stoller. 2009. Parametric heap usage analysis for functional programs. In International Symposium on Memory Management. 139\u2013148. https:\/\/www3.cs.stonybrook.edu\/~stoller\/papers\/ismm2009.pdf"},{"key":"e_1_2_2_60_1","doi-asserted-by":"crossref","unstructured":"Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael-Scott queue. In Certified Programs and Proofs (CPP). 76\u201390. https:\/\/cs.au.dk\/~birke\/papers\/2021-ms-queue-final.pdf Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael-Scott queue. In Certified Programs and Proofs (CPP). 76\u201390. https:\/\/cs.au.dk\/~birke\/papers\/2021-ms-queue-final.pdf","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360597"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498672","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498672","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T15:30:28Z","timestamp":1750174228000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498672"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498672"],"URL":"https:\/\/doi.org\/10.1145\/3498672","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}