{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:53:45Z","timestamp":1725537225400},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040269"},{"type":"electronic","value":"9783642040276"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04027-6_32","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T13:27:52Z","timestamp":1252934872000},"page":"440-454","source":"Crossref","is-referenced-by-count":21,"title":["Nested Hoare Triples and Frame Rules for Higher-Order Store"],"prefix":"10.1007","author":[{"given":"Jan","family":"Schwinghammer","sequence":"first","affiliation":[]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Reus","sequence":"additional","affiliation":[]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"32_CR1","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0022-0000(89)90027-5","volume":"39","author":"P. America","year":"1989","unstructured":"America, P., Rutten, J.J.M.M.: Solving reflexive domain equations in a category of complete metric spaces. J. Comput. Syst. Sci.\u00a039(3), 343\u2013375 (1989)","journal-title":"J. Comput. Syst. Sci."},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-70583-3_29","volume-title":"Automata, Languages and Programming","author":"L. Birkedal","year":"2008","unstructured":"Birkedal, L., Reus, B., Schwinghammer, J., Yang, H.: A simple model of separation logic for higher-order store. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 348\u2013360. Springer, Heidelberg (2008)"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/978-3-642-00596-1_32","volume-title":"FOSSACS 2009","author":"L. Birkedal","year":"2009","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: Realizability semantics of parametric polymorphism, general references, and recursive types. In: FOSSACS 2009. LNCS, vol.\u00a05504, pp. 456\u2013470. Springer, Heidelberg (2009)"},{"key":"32_CR4","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. Log. Methods Comput. Sci.\u00a02(5:1) (2006)","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"32_CR5","first-page":"270","volume-title":"LICS","author":"K. Honda","year":"2005","unstructured":"Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: LICS, pp. 270\u2013279. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"32_CR6","unstructured":"Krishnaswami, N., Birkedal, L., Aldrich, J., Reynolds, J.: Idealized ML and Its Separation Logic (2007), http:\/\/www.cs.cmu.edu\/~neelk\/"},{"key":"32_CR7","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/1411204.1411237","volume-title":"ICFP","author":"A. Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: ICFP, pp. 229\u2013240. ACM Press, New York (2008)"},{"issue":"2","key":"32_CR8","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P.W. O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. B. Symb. Log.\u00a05(2), 215\u2013244 (1999)","journal-title":"B. Symb. Log."},{"key":"32_CR9","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/1328438.1328451","volume-title":"POPL","author":"M. Parkinson","year":"2008","unstructured":"Parkinson, M., Biermann, G.: Separation logic, abstraction and inheritance. In: POPL, pp. 75\u201386. ACM Press, New York (2008)"},{"key":"32_CR10","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. Inf. Comput.\u00a0127, 66\u201390 (1996)","journal-title":"Inf. Comput."},{"key":"32_CR11","first-page":"331","volume-title":"LICS","author":"F. Pottier","year":"2008","unstructured":"Pottier, F.: Hiding local state in direct style: a higher-order anti-frame rule. In: LICS, pp. 331\u2013340. IEEE Computer Society Press, Los Alamitos (2008)"},{"key":"32_CR12","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":"32_CR13","first-page":"55","volume-title":"LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"issue":"4","key":"32_CR14","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1137\/0211062","volume":"11","author":"M.B. Smyth","year":"1982","unstructured":"Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM J. Comput.\u00a011(4), 761\u2013783 (1982)","journal-title":"SIAM J. Comput."},{"key":"32_CR15","doi-asserted-by":"publisher","DOI":"10.1142\/6284","volume-title":"Domain-theoretic Foundations of Functional Programming","author":"T. Streicher","year":"2006","unstructured":"Streicher, T.: Domain-theoretic Foundations of Functional Programming. World Scientific, Singapore (2006)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T15:07:47Z","timestamp":1685113667000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}