{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:23Z","timestamp":1772164043347,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,1,23]],"date-time":"2013-01-23T00:00:00Z","timestamp":1358899200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,1,23]]},"DOI":"10.1145\/2429069.2429105","type":"proceedings-article","created":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T10:29:29Z","timestamp":1358850569000},"page":"301-314","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["High-level separation logic for low-level code"],"prefix":"10.1145","author":[{"given":"Jonas B.","family":"Jensen","sequence":"first","affiliation":[{"name":"IT University, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nick","family":"Benton","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Kennedy","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,1,23]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.003"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_2_2_4_1","volume-title":"Proc. of ITP","author":"Bengtson J.","year":"2012","unstructured":"J. Bengtson , J. B. Jensen , and L. Birkedal . Charge! -- a framework for higher-order separation logic in Coq . In Proc. of ITP , 2012 . J. Bengtson, J. B. Jensen, and L. Birkedal. Charge! -- a framework for higher-order separation logic in Coq. In Proc. of ITP, 2012."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_24"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11874683_12"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481864"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.47"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(2:6)2008"},{"key":"e_1_3_2_2_11_1","volume-title":"3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO 2011)","author":"Blanqui F.","year":"2011","unstructured":"F. Blanqui , C. Helmstetter , V. Joloboff , J.-F. Monin , and X. Shi . Designing a CPU model: from a pseudo-formal document to fast code . In 3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO 2011) , 2011 . F. Blanqui, C. Helmstetter, V. Joloboff, J.-F. Monin, and X. Shi. Designing a CPU model: from a pseudo-formal document to fast code. In 3rd Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools (RAPIDO 2011), 2011."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_2_2_13_1","first-page":"7","author":"Burstall R. M.","year":"1972","unstructured":"R. M. Burstall . Some techniques for proving correctness of programs which alter data structures. Machine Intelligence , 7 , 1972 . R. M. Burstall. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence, 7, 1972.","journal-title":"Machine Intelligence"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250743"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_2_17_1","volume-title":"Certified Programming with Dependent Types","author":"Chlipala A.","unstructured":"A. Chlipala . Certified Programming with Dependent Types . MIT Press , to appear. A. Chlipala. Certified Programming with Dependent Types. MIT Press, to appear."},{"key":"e_1_3_2_2_18_1","series-title":"Proc","volume-title":"Mathematical Aspects of Computer Science","author":"Floyd R. W.","year":"1967","unstructured":"R. W. Floyd . Assigning meanings to programs . In J. T. Schwartz, editor, Mathematical Aspects of Computer Science , volume 19 of Proc . of Symposia in Applied Mathematics, Providence, Rhode Island , 1967 . AMS. R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia in Applied Mathematics, Providence, Rhode Island, 1967. AMS."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480935"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_3_2_2_24_1","series-title":"Proc","volume-title":"Mathematical Aspects of Computer Science","author":"McCarthy J.","year":"1967","unstructured":"J. McCarthy and J. Painter . Correctness of a compiler for arithmetic expressions . In Mathematical Aspects of Computer Science , volume 19 of Proc . of Symposia in Applied Mathematics. AMS , 1967 . J. McCarthy and J. Painter. Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, volume 19 of Proc. of Symposia in Applied Mathematics. AMS, 1967."},{"key":"e_1_3_2_2_25_1","first-page":"5","author":"Moore J. Strother","year":"1989","unstructured":"J. Strother Moore . A mechanically verified language implementation. Journal of Automated Reasoning , 5 , 1989 . J. Strother Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254111"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706313"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763565"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789002"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111066"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964024"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.16"},{"key":"e_1_3_2_2_34_1","volume-title":"Logics of Programs","author":"Reynolds J. C.","year":"1983","unstructured":"J. C. Reynolds . An introduction to specification logic . In Logics of Programs , 1983 . J. C. Reynolds. An introduction to specification logic. In Logics of Programs, 1983."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.020"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_6"},{"key":"e_1_3_2_2_39_1","volume-title":"Report of a Conference on High Speed Automatic Calculating Machines","author":"Turing A. M.","year":"1949","unstructured":"A. M. Turing . Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines , 1949 . A. M. Turing. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, 1949."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2011.16"},{"key":"e_1_3_2_2_41_1","first-page":"5","author":"Young W. D.","year":"1989","unstructured":"W. D. Young . A mechanically verified code generator. Journal of Automated Reasoning , 5 , 1989 . W. D. Young. A mechanically verified code generator. Journal of Automated Reasoning, 5, 1989.","journal-title":"Journal of Automated Reasoning"}],"event":{"name":"POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Rome Italy","acronym":"POPL '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429105","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2429069.2429105","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:35Z","timestamp":1750221335000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2429069.2429105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,23]]},"references-count":39,"alternative-id":["10.1145\/2429069.2429105","10.1145\/2429069"],"URL":"https:\/\/doi.org\/10.1145\/2429069.2429105","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2480359.2429105","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,1,23]]},"assertion":[{"value":"2013-01-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}