{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:37:10Z","timestamp":1750307830942,"version":"3.41.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2008,7,1]],"date-time":"2008-07-01T00:00:00Z","timestamp":1214870400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Danish Natural Science Research Council","award":["51--00--0315"],"award-info":[{"award-number":["51--00--0315"]}]},{"DOI":"10.13039\/100008393","name":"Danish Technical Research Council","doi-asserted-by":"crossref","award":["56--00--0309"],"award-info":[{"award-number":["56--00--0309"]}],"id":[{"id":"10.13039\/100008393","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0204242"],"award-info":[{"award-number":["CCR-0204242"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2008,7]]},"abstract":"<jats:p>We present a programming language, model, and logic appropriate for implementing and reasoning about a memory management system. We state semantically what is meant by correctness of a copying garbage collector, and employ a variant of the novel separation logics to formally specify partial correctness of Cheney's copying garbage collector in our program logic. Finally, we prove that our implementation of Cheney's algorithm meets its specification using the logic we have given and auxiliary variables.<\/jats:p>","DOI":"10.1145\/1377492.1377499","type":"journal-article","created":{"date-parts":[[2008,8,5]],"date-time":"2008-08-05T13:35:10Z","timestamp":1217943310000},"page":"1-58","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Local reasoning about a copying garbage collector"],"prefix":"10.1145","volume":"30","author":[{"given":"Noah","family":"Torp-Smith","sequence":"first","affiliation":[{"name":"IT University of Copenhagen"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John C.","family":"Reynolds","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,8]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1145\/165180.165192"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/182409.182414"},{"volume-title":"Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03)","author":"Ahmed A.","key":"e_1_2_1_3_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.5555\/871816.871860"},{"unstructured":"Appel A. W. and Gon\u00e7alves M. J. R. 1993. Hash-consing garbage collection. Tech. rep. CS-TR-412-93 Princeton University.]]  Appel A. W. and Gon\u00e7alves M. J. R. 1993. Hash-consing garbage collection. Tech. rep. CS-TR-412-93 Princeton University.]]","key":"e_1_2_1_5_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/579.587"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1007\/11575467_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1007\/978-3-540-31987-0_17"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/964001.964020"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1109\/LICS.2005.47"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.5555\/648085.747307"},{"unstructured":"Bornat R. 2003. Correctness of copydag via local reasoning. Private Communication.]]  Bornat R. 2003. Correctness of copydag via local reasoning. Private Communication.]]","key":"e_1_2_1_12_1"},{"volume-title":"Proceedings of the Conference on Semantics, Program Analysis, and Computing Environments (SPACE'04)","year":"2004","author":"Bornat R.","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'01)","volume":"2152","author":"Burdy L.","year":"2001"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/351268.351291"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1016\/S0304-3975(02)00868-X"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/362790.362798"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1093\/logcom\/13.6.815"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1145\/292540.292564"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/359642.359655"},{"volume-title":"Informal Proceedings of the 2nd Workshop on Semantics, Program Analysis and Computing Environments for Memory Management (SPACE'04)","author":"Fluet M.","key":"e_1_2_1_21_1"},{"unstructured":"Goto E. 1974. Monocopy and associative algorithms in extended lisp. Tech. rep. TR 74-03 University of Tokyo.]]  Goto E. 1974. Monocopy and associative algorithms in extended lisp. Tech. rep. TR 74-03 University of Tokyo.]]","key":"e_1_2_1_22_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1145\/357114.357119"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.1007\/BF01128406"},{"unstructured":"Guttmann J. D. Monk L. G. Ramsdell J. D. Farmer W. M. and Swarup V. 1992. A guide to VLISP a verified programming language implementation. Tech. rep. M92B091 The MITRE Corporation.]]  Guttmann J. D. Monk L. G. Ramsdell J. D. Farmer W. M. and Swarup V. 1992. A guide to VLISP a verified programming language implementation. Tech. rep. M92B091 The MITRE Corporation.]]","key":"e_1_2_1_25_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1145\/512529.512547"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.5555\/645611.662365"},{"volume-title":"Proceedings of the Conference on Semantics, Program Analysis, and Computing Environments (SPACE'04)","author":"Hawblitzel C.","key":"e_1_2_1_28_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/363235.363259"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.5555\/646525.694869"},{"volume-title":"Proceedings of the USENIX Annual Technical Conference","author":"Jim T.","key":"e_1_2_1_31_1"},{"volume-title":"Proceedings of the Conference on Automated Deduction (CADE-19)","author":"Mehta F.","key":"e_1_2_1_32_1"},{"unstructured":"Monnier S. and Shao Z. 2002. Typed regions. Tech. rep. YALEU\/DCS\/TR-1242 Department of Computer Science Yale University New Haven CT.]]  Monnier S. and Shao Z. 2002. Typed regions. Tech. rep. YALEU\/DCS\/TR-1242 Department of Computer Science Yale University New Haven CT.]]","key":"e_1_2_1_33_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1145\/224164.224182"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1145\/319301.319345"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1145\/263699.263712"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1145\/238721.238781"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04)","volume":"3170","author":"O'Hearn P. W.","year":"2004"},{"volume-title":"Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'01)","author":"O'Hearn P. W.","key":"e_1_2_1_39_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1007\/BF00268134"},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1145\/604131.604147"},{"doi-asserted-by":"publisher","key":"e_1_2_1_42_1","DOI":"10.1007\/BF01788566"},{"doi-asserted-by":"crossref","unstructured":"Pym D. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logics Series. vol. 26 Kluwer.]]  Pym D. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logics Series. vol. 26 Kluwer.]]","key":"e_1_2_1_43_1","DOI":"10.1007\/978-94-017-0091-7"},{"unstructured":"Reynolds J. C. 1981. The Craft of Programming. Prentice-Hall International Series in Computer Science. Prentice-Hall.]]   Reynolds J. C. 1981. The Craft of Programming. Prentice-Hall International Series in Computer Science. Prentice-Hall.]]","key":"e_1_2_1_44_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.5555\/645683.664578"},{"doi-asserted-by":"publisher","key":"e_1_2_1_46_1","DOI":"10.1007\/BF01211305"},{"volume-title":"Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP'00)","author":"Smith F.","key":"e_1_2_1_47_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_48_1","DOI":"10.1145\/1040305.1040321"},{"unstructured":"Swarup V. Farmer W. M. Guttmann J. D. Monk L. G. and Ramsdell J. D. 1992. The VLISP byte-code interpreter. Tech. rep. M 92B096 The MITRE Corporation.]]  Swarup V. Farmer W. M. Guttmann J. D. Monk L. G. and Ramsdell J. D. 1992. The VLISP byte-code interpreter. Tech. rep. M 92B096 The MITRE Corporation.]]","key":"e_1_2_1_49_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_50_1","DOI":"10.1145\/291891.291894"},{"doi-asserted-by":"publisher","key":"e_1_2_1_51_1","DOI":"10.1023\/B:LISP.0000029446.78563.a4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_52_1","DOI":"10.1145\/174675.177855"},{"doi-asserted-by":"publisher","key":"e_1_2_1_53_1","DOI":"10.1145\/360336.360338"},{"doi-asserted-by":"publisher","key":"e_1_2_1_54_1","DOI":"10.1145\/360204.360218"},{"doi-asserted-by":"publisher","key":"e_1_2_1_55_1","DOI":"10.1007\/978-3-540-30124-0_21"},{"unstructured":"Yang H. 2001. Local reasoning for stateful programs. Ph. D. thesis University of Illinois Urbana-Champaign.]]   Yang H. 2001. Local reasoning for stateful programs. Ph. D. thesis University of Illinois Urbana-Champaign.]]","key":"e_1_2_1_56_1"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1377492.1377499","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1377492.1377499","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:57:55Z","timestamp":1750255075000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1377492.1377499"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7]]},"references-count":56,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["10.1145\/1377492.1377499"],"URL":"https:\/\/doi.org\/10.1145\/1377492.1377499","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2008,7]]},"assertion":[{"value":"2004-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2006-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-08-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}