{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T23:33:16Z","timestamp":1761953596276,"version":"build-2065373602"},"reference-count":20,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2008,10,1]],"date-time":"2008-10-01T00:00:00Z","timestamp":1222819200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":1762,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2008,10]]},"DOI":"10.1016\/j.entcs.2008.10.022","type":"journal-article","created":{"date-parts":[[2008,10,22]],"date-time":"2008-10-22T09:56:42Z","timestamp":1224669402000},"page":"371-389","source":"Crossref","is-referenced-by-count":10,"special_numbering":"C","title":["Higher-Order Separation Logic in Isabelle\/HOLCF"],"prefix":"10.1016","volume":"218","author":[{"given":"Carsten","family":"Varming","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.entcs.2008.10.022_bib001","doi-asserted-by":"crossref","DOI":"10.1145\/1275497.1275499","article-title":"BI-hyperdoctrines, higher-order separation logic, and abstraction","volume":"29","author":"Biering","year":"2007","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.entcs.2008.10.022_bib002","doi-asserted-by":"crossref","unstructured":"Birkedal, L., N.T. Smith and J.C. Reynolds, Local reasoning about a copying garbage collector, in: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2004), pp. 220\u2013231","DOI":"10.1145\/964001.964020"},{"key":"10.1016\/j.entcs.2008.10.022_bib003","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","article-title":"A semantics for concurrent separation logic","volume":"375","author":"Brookes","year":"2007","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.entcs.2008.10.022_bib004","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1145\/362790.362798","article-title":"A nonrecursive list compacting algorithm","volume":"13","author":"Cheney","year":"1970","journal-title":"Commun. ACM"},{"key":"10.1016\/j.entcs.2008.10.022_bib005","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/j.entcs.2008.10.022_bib006","doi-asserted-by":"crossref","unstructured":"Gordon, M., Introduction to the HOL system, in: HOL Theorem Proving System and Its Applications, 1991., International Workshop on the, 1991, pp. 2\u20133","DOI":"10.1109\/HOL.1991.596265"},{"key":"10.1016\/j.entcs.2008.10.022_bib007","unstructured":"Krishnaswami, N., J. Aldrich and L. Birkedal, Modular verification of the Subject-Observer pattern via higher-order separation logic, in: 9th Workshop on Formal Techniques for Java-like Programs (FTfJP 2007), 2007"},{"key":"10.1016\/j.entcs.2008.10.022_bib008","doi-asserted-by":"crossref","unstructured":"Lin, C., A. Mccreight, Z. Shao, Y. Chen and Y. Guo, Foundational typed assembly language with certified garbage collection, in: TASE '07: Proceedings of the First Joint IEEE\/IFIP Symposium on Theoretical Aspects of Software Engineering (2007), pp. 326\u2013338","DOI":"10.1109\/TASE.2007.28"},{"key":"10.1016\/j.entcs.2008.10.022_bib009","doi-asserted-by":"crossref","first-page":"468","DOI":"10.1145\/1273442.1250788","article-title":"A general framework for certifying garbage collectors and their mutators","volume":"42","author":"McCreight","year":"2007","journal-title":"SIGPLAN Not."},{"key":"10.1016\/j.entcs.2008.10.022_bib010","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1017\/S095679689900341X","article-title":"HOLCF = HOL + LCF","volume":"9","author":"M\u00fcller","year":"1999","journal-title":"J. Funct. Program."},{"key":"10.1016\/j.entcs.2008.10.022_bib011","series-title":"Proceedings of ESOP'07","first-page":"189","article-title":"Abstract Predicates and Mutable ADTs in Hoare Type Theory","volume":"4421","author":"Nanevski","year":"2007"},{"key":"10.1016\/j.entcs.2008.10.022_bib012","article-title":"Resources, concurrency, and local reasoning","volume":"375","author":"O'Hearn","year":"2007","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/j.entcs.2008.10.022_bib013","unstructured":"O'Hearn, P.W., J.C. Reynolds and H. Yang, Local reasoning about programs that alter data structures, in: CSL'01: Proceedings of the 15th International Workshop on Computer Science Logic (2001), pp. 1\u201319"},{"key":"10.1016\/j.entcs.2008.10.022_bib014","unstructured":"Parkinson, M., When separation logic met Java, in: FTfJP'06, 2006"},{"key":"10.1016\/j.entcs.2008.10.022_bib015","doi-asserted-by":"crossref","unstructured":"Parkinson, M. and G. Biermann, Separation logic, abstraction and inheritance, in: Proc. 35th POPL, 2008","DOI":"10.1145\/1328438.1328451"},{"key":"10.1016\/j.entcs.2008.10.022_bib016","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Isabelle: The next seven hundred theorem provers, in: Proceedings of the 9th International Conference on Automated Deduction (1988), pp. 772\u2013773","DOI":"10.1007\/BFb0012891"},{"key":"10.1016\/j.entcs.2008.10.022_bib017","doi-asserted-by":"crossref","unstructured":"Preoteasa, V., Mechanical verification of recursive procedures manipulating pointers using separation logic, in: 14th International Symposium on Formal Methods, 2006, pp. 508\u2013523","DOI":"10.1007\/11813040_34"},{"year":"2002","series-title":"Separation logic: A logic for shared mutable data structures","author":"Reynolds","key":"10.1016\/j.entcs.2008.10.022_bib018"},{"key":"10.1016\/j.entcs.2008.10.022_bib019","series-title":"Proceedings of CSL'04","first-page":"250","article-title":"Towards mechanized program verification with separation logic","volume":"3210","author":"Weber","year":"2004"},{"year":"2002","series-title":"An example of local reasoning in BI pointer logic: the Schorr-Waite graph marking algorithm","author":"Yang","key":"10.1016\/j.entcs.2008.10.022_bib020"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066108004167?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066108004167?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,2,2]],"date-time":"2025-02-02T05:19:53Z","timestamp":1738473593000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066108004167"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10]]},"references-count":20,"alternative-id":["S1571066108004167"],"URL":"https:\/\/doi.org\/10.1016\/j.entcs.2008.10.022","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2008,10]]}}}