{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:44Z","timestamp":1780994804607,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705826","type":"print"},{"value":"9783540705833","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70583-3_29","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"348-360","source":"Crossref","is-referenced-by-count":15,"title":["A Simple Model of Separation Logic for Higher-Order Store"],"prefix":"10.1007","author":[{"given":"Lars","family":"Birkedal","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bernhard","family":"Reus","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"Schwinghammer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM TOPLAS\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275499"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for algol-like languages. LMCS\u00a02(5-1) (2006)","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_8","volume-title":"Foundations of Software Science and Computational Structures","author":"L. Birkedal","year":"2007","unstructured":"Birkedal, L., Yang, H.: Relational parametricity and separation logic. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol.\u00a04423. Springer, Heidelberg (2007)"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: Proc. PLDI 2007, pp. 66\u201377 (2007)","DOI":"10.1145\/1250734.1250743"},{"key":"29_CR5","volume-title":"Linux Device Drivers","author":"J. Corbet","year":"2005","unstructured":"Corbet, J., Rubini, A., Kroah-Hartman, G.: Linux Device Drivers, 3rd edn. O\u2019Reilly, Sebastopol (2005)","edition":"3"},{"key":"29_CR6","unstructured":"Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: Proc. LICS 2005, pp. 270\u2013279 (2005)"},{"key":"29_CR7","unstructured":"Krishnaswami, N., Aldrich, J., Birkedal, L.: Modular verification of the subject-observer pattern via higher-order separation logic. In: FTfJP 2007 (2007)"},{"key":"29_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-71316-6_14","volume-title":"Programming Languages and Systems","author":"A. Nanevski","year":"2007","unstructured":"Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract predicates and mutable ADTs in Hoare type theory. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 189\u2013204. Springer, Heidelberg (2007)"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: Proc. ICFP 2006, pp. 62\u201373 (2006)","DOI":"10.1145\/1159803.1159812"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201318. Springer, Heidelberg (2001)"},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proc. of 31st POPL, pp. 268\u2013280 (2004)","DOI":"10.1145\/982962.964024"},{"key":"29_CR12","unstructured":"Parkinson, M.: When separation logic met Java. In: FTfJP 2006 (2006)"},{"key":"29_CR13","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Proc. 35th POPL (2008)","DOI":"10.1145\/1328438.1328451"},{"key":"29_CR14","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1006\/inco.1996.0052","volume":"127","author":"A.M. Pitts","year":"1996","unstructured":"Pitts, A.M.: Relational properties of domains. Information and Computation\u00a0127, 66\u201390 (1996)","journal-title":"Information and Computation"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/11874683_38","volume-title":"Computer Science Logic","author":"B. Reus","year":"2006","unstructured":"Reus, B., Schwinghammer, J.: Separation logic for higher-order store. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol.\u00a04207, pp. 575\u2013590. Springer, Heidelberg (2006)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1337","DOI":"10.1007\/11523468_108","volume-title":"Automata, Languages and Programming","author":"B. Reus","year":"2005","unstructured":"Reus, B., Streicher, T.: About Hoare logics for higher-order store. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1337\u20131348. Springer, Heidelberg (2005)"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70583-3_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:07:58Z","timestamp":1605744478000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70583-3_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705826","9783540705833"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70583-3_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}