{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:18:42Z","timestamp":1759033122295,"version":"3.41.2"},"reference-count":32,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,9,28]],"date-time":"2011-09-28T00:00:00Z","timestamp":1317168000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/G003173\/1"],"award-info":[{"award-number":["EP\/G003173\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/E053041\/1"],"award-info":[{"award-number":["EP\/E053041\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/H008373\/1"],"award-info":[{"award-number":["EP\/H008373\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level languages with ML-style general (higher-order) storage, we investigate the compatibility of nested Hoare triples with several variations of higher-order frame rules. The interaction of nested triples and frame rules can be subtle, and the inclusion of certain frame rules is in fact unsound. A particular combination of rules can be shown consistent by means of a Kripke model where worlds live in a recursively defined ultrametric space. The resulting logic allows us to elegantly prove programs involving stored code. In particular, using recursively defined assertions, it leads to natural specifications and proofs of invariants required for dealing with recursion through the store.<\/jats:p>","DOI":"10.2168\/lmcs-7(3:21)2011","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T13:45:24Z","timestamp":1415972724000},"source":"Crossref","is-referenced-by-count":6,"title":["Nested Hoare Triples and Frame Rules for Higher-order Store"],"prefix":"10.46298","volume":"Volume 7, Issue 3","author":[{"given":"Jan","family":"Schwinghammer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5807-856X","authenticated-orcid":false,"given":"Bernhard","family":"Reus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,9,28]]},"reference":[{"issue":"3","key":"10.2168\/LMCS-7(3:21)2011_America-Rutten:JCSS89","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0022-0000(89)90027-5","volume":"39","author":"P. America and J. J. M. M. Rutten","year":"1989","journal-title":"J. Comput. Syst. Sci."},{"issue":"5","key":"10.2168\/LMCS-7(3:21)2011_Appel:McAllester:01","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"A. W. Appel and D. A. McAllester","year":"2001","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.2168\/LMCS-7(3:21)2011_Benton:06","doi-asserted-by":"crossref","unstructured":"N. Benton. Abstracting allocation. InProceedings of CSL, pages 182-196, 2006.","DOI":"10.1007\/11874683_12"},{"key":"10.2168\/LMCS-7(3:21)2011_BirkedalRSSTY11","doi-asserted-by":"crossref","unstructured":"L. Birkedal, B. Reus, J. Schwinghammer, K. St\u00f8vring, J. Thamsborg, and H. Yang. Step-indexed Kripke models over recursive worlds. InProceedings of POPL, pages 119-132, 2011.","DOI":"10.1145\/1925844.1926401"},{"key":"10.2168\/LMCS-7(3:21)2011_Birkedal:Reus:Schwinghammer:Yang:08","doi-asserted-by":"crossref","unstructured":"L. Birkedal, B. Reus, J. Schwinghammer, and H. Yang. A simple model of separation logic for higher-order store. InProceedings of ICALP, pages 348-360, 2008.","DOI":"10.1007\/978-3-540-70583-3_29"},{"key":"10.2168\/LMCS-7(3:21)2011_Birkedal:Stovring:Thamsborg:09","doi-asserted-by":"crossref","unstructured":"L. Birkedal, K. St\u00f8vring, and J. Thamsborg. Realizability semantics of parametric polymorphism, general references, and recursive types. InProceedings of FOSSACS, pages 456-470, 2009.","DOI":"10.1007\/978-3-642-00596-1_32"},{"key":"10.2168\/LMCS-7(3:21)2011_BirkedalL:semslt-lmcs","first-page":"1","volume":"5","author":"L. Birkedal, N. Torp-Smith, and H. Yang","year":"2006","journal-title":"Logical Methods in Computer Science"},{"key":"10.2168\/LMCS-7(3:21)2011_Birkedal:Yang:parsepl-journal","first-page":"6","volume":"2","author":"L. Birkedal and H. Yang","year":"2008","journal-title":"Logical Methods in Computer Science"},{"key":"10.2168\/LMCS-7(3:21)2011_Crowfoot11","doi-asserted-by":"crossref","unstructured":"N. Charlton, B. Horsfall, and B. Reus. Crowfoot: a verifier for higher order store programs. Unpublished, available at http:\/\/www.informatics.sussex.ac.uk\/research\/projects\/PL4HOStore\/, Feb. 2011.","DOI":"10.1007\/978-3-642-27940-9_10"},{"key":"10.2168\/LMCS-7(3:21)2011_CharltonReusLola10","unstructured":"N. Charlton and B. Reus. A deeper understanding of the deep frame axiom (extended abstract). Presented at LOLA Workshop 2010 (Syntax and Semantics of Low Level Languages), July 2010."},{"key":"10.2168\/LMCS-7(3:21)2011_Charlton:Reus:11","doi-asserted-by":"crossref","unstructured":"N. Charlton and B. Reus. Specification patterns and proofs for recursion through the store. InProceedings of FCT, 2011.","DOI":"10.1007\/978-3-642-22953-4_27"},{"key":"10.2168\/LMCS-7(3:21)2011_Honda:Yoshida:Berger:05","unstructured":"K. Honda, N. Yoshida, and M. Berger. An observationally complete program logic for imperative higher-order functions. InProceedings of LICS, pages 270-279, 2005."},{"key":"10.2168\/LMCS-7(3:21)2011_Krishnaswami:ML-SL07","unstructured":"N. Krishnaswami, L. Birkedal, J. Aldrich, and J. C. Reynolds. Idealized ML and Its Separation Logic. Available at http:\/\/www.cs.cmu.edu\/ neelk\/, 2007."},{"key":"10.2168\/LMCS-7(3:21)2011_Nanevski:Morrisett:Shinnar:Govereau:Birkedal:08","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"issue":"2","key":"10.2168\/LMCS-7(3:21)2011_OHearn:Pym:99","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P. W. O'Hearn and D. J. Pym","year":"1999","journal-title":"B. Symb. Log."},{"key":"10.2168\/LMCS-7(3:21)2011_OHearn:Yang:Reynolds:04","doi-asserted-by":"crossref","unstructured":"P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. InProceedings of POPL, pages 268-280, 2004.","DOI":"10.1145\/964001.964024"},{"key":"10.2168\/LMCS-7(3:21)2011_Parkinson:Biermann:08","doi-asserted-by":"crossref","unstructured":"M. Parkinson and G. Biermann. Separation logic, abstraction and inheritance. InProceedings of POPL, pages 75-86, 2008.","DOI":"10.1145\/1328438.1328451"},{"key":"10.2168\/LMCS-7(3:21)2011_Pierce:02","unstructured":"B. C. Pierce.Types and Programming Languages. MIT Press, 2002."},{"key":"10.2168\/LMCS-7(3:21)2011_Pitts:96","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A. M. Pitts","year":"1996","journal-title":"Inf. Comput."},{"journal-title":"In Proceedings of LICS","author":"F. Pottier","key":"10.2168\/LMCS-7(3:21)2011_Pottier:08"},{"journal-title":"Unpublished, July 2009","author":"F. Pottier","key":"10.2168\/LMCS-7(3:21)2011_Pottier09"},{"issue":"1","key":"10.2168\/LMCS-7(3:21)2011_Pym:OHearn:Yang:04","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/j.tcs.2003.11.020","volume":"315","author":"D. J. Pym, P. W. O'Hearn, and H. Yan","year":"2004","journal-title":"Theor. Comput. Sci."},{"key":"10.2168\/LMCS-7(3:21)2011_Reus:Schwinghammer:06","doi-asserted-by":"crossref","unstructured":"B. Reus and J. Schwinghammer. Separation logic for higher-order store. InProceedings of CSL, pages 575-590, 2006.","DOI":"10.1007\/11874683_38"},{"key":"10.2168\/LMCS-7(3:21)2011_Reynolds:82","unstructured":"J. C. Reynolds. Idealized Algol and its specification logic. In D. N\u00e9el, editor,Tools and Notions for Program Construction, pages 121-161. Cambridge University Press, 1982."},{"key":"10.2168\/LMCS-7(3:21)2011_Reynolds:02a","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Separation logic: A logic for shared mutable data structures. InProceedings of LICS, pages 55-74, 2002.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"10.2168\/LMCS-7(3:21)2011_schwinghammerBRY09","doi-asserted-by":"crossref","unstructured":"J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested Hoare triples and frame rules for higher-order store. InProceedings of CSL, pages 440-454, 2009.","DOI":"10.1007\/978-3-642-04027-6_32"},{"key":"10.2168\/LMCS-7(3:21)2011_Schwinghammer:Birkedal:Stovring:11","doi-asserted-by":"crossref","unstructured":"J. Schwinghammer, L. Birkedal, and K. St\u00f8vring. A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. InProceedings of FOSSACS, pages 305-319, 2011.","DOI":"10.1007\/978-3-642-19805-2_21"},{"key":"10.2168\/LMCS-7(3:21)2011_schwinghammerYBPR10","doi-asserted-by":"crossref","unstructured":"J. Schwinghammer, H. Yang, L. Birkedal, F. Pottier, and B. Reus. A semantic foundation for hidden state. InProceedings of FOSSACS, pages 2-17, 2010.","DOI":"10.1007\/978-3-642-12032-9_2"},{"issue":"4","key":"10.2168\/LMCS-7(3:21)2011_Plotkin:Smyth:82","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1137\/0211062","volume":"11","author":"M. B. Smyth and G. D. Plotkin","year":"1982","journal-title":"SIAM J. Comput."},{"key":"10.2168\/LMCS-7(3:21)2011_Sorensen:Urzyczyn:06","doi-asserted-by":"crossref","unstructured":"M. H. S\u00f8rensen and P. Urzyczyn.Lectures on the Curry-Howard Isomorphism, volume 149 ofStudies in Logic and the Foundations of Mathematics. Elsevier, 2006.","DOI":"10.1016\/S0049-237X(06)80005-4"},{"key":"10.2168\/LMCS-7(3:21)2011_Streicher:06","doi-asserted-by":"crossref","unstructured":"T. Streicher.Domain-theoretic Foundations of Functional Programming. World Scientific, 2006.","DOI":"10.1142\/6284"},{"key":"10.2168\/LMCS-7(3:21)2011_Honda:Yoshida:Berger:07","doi-asserted-by":"crossref","unstructured":"N. Yoshida, K. Honda, and M. Berger. Logical reasoning for higher-order functions with local state. InFoundations of Software Science and Computation Structure, pages 361-377, 2007.","DOI":"10.1007\/978-3-540-71389-0_26"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/996\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/996\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T18:03:36Z","timestamp":1747159416000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/996"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,28]]},"references-count":32,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(3:21)2011","relation":{"references":[{"id-type":"doi","id":"10.1007\/978-3-540-70583-3_29","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1109.3031","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1109.3031","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,9,28]]},"article-number":"996"}}