{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:32:59Z","timestamp":1742963579603,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642228629"},{"type":"electronic","value":"9783642228636"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_5","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"22-38","source":"Crossref","is-referenced-by-count":15,"title":["Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq"],"prefix":"10.1007","author":[{"given":"Jesper","family":"Bengtson","sequence":"first","affiliation":[]},{"given":"Jonas Braband","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Filip","family":"Sieczkowski","sequence":"additional","affiliation":[]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8598-9","volume-title":"A Theory of Objects","author":"M. Abadi","year":"1996","unstructured":"Abadi, M., Cardelli, L.: A Theory of Objects, 1st edn. Springer, New York (1996)","edition":"1"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Melli\u00e8s, P.-A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proceedings of POPL (2007)","DOI":"10.1145\/1190216.1190235"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-31987-0_17","volume-title":"Programming Languages and Systems","author":"B. Biering","year":"2005","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI hyperdoctrines and higher-order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 233\u2013247. Springer, Heidelberg (2005)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275499"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Reus, B., Schwinghammer, J., St\u00f8vring, K., Thamsborg, J., Yang, H.: Step-indexed kripke models over recursive worlds. In: Proceedings of POPL (2011)","DOI":"10.1145\/1926385.1926401"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Proceedings of LICS, pp. 366\u2013378 (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"#cr-split#-5_CR7.1","doi-asserted-by":"crossref","unstructured":"Jensen, J., Birkedal, L., Sestoft, P.: Modular verification of linked lists with views via separation logic. Journal of Object Technology (2011);","DOI":"10.5381\/jot.2011.10.1.a2"},{"key":"#cr-split#-5_CR7.2","unstructured":"To Appear Preliminary version in FTfJP 2010, http:\/\/www.itu.dk\/people\/birkedal\/papers\/views.pdf"},{"key":"5_CR8","unstructured":"Kokholm, N., Sestoft, P.: The C5 generic collection library for C# and CLI. Technical Report ITU-TR-2006-76, IT University of Copenhagen (2006)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Aldrich, J., Birkedal, L., Svendsen, K., Buisse, A.: Design patterns in separation logic. In: Proceedings of TLDI, pp. 105\u2013116 (2009)","DOI":"10.1145\/1481861.1481874"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-642-20398-5_42","volume-title":"NASA Formal Methods","author":"H. Mehnert","year":"2011","unstructured":"Mehnert, H.: Kopitiam: Modular incremental interactive full functional static verification of java code. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 518\u2013524. Springer, Heidelberg (2011)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"ESOP","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, Springer, Heidelberg (2007)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"CSL","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\u201319. Springer, Heidelberg (2001)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Proceedings of POPL, pp. 247\u2013258 (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: Proceedings of POPL, pp. 75\u201386 (2008)","DOI":"10.1145\/1328438.1328451"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Preoteasa, V.: Frame rules for mutually recursive procedures manipulating pointers. Theoretical Computer Science (2009)","DOI":"10.1016\/j.tcs.2009.05.016"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/978-3-642-04027-6_32","volume-title":"CSL","author":"J. Schwinghammer","year":"2009","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare triples and frame rules for higher-order store. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 440\u2013454. Springer, Heidelberg (2009)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-642-14107-2_9","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"K. Svendsen","year":"2010","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Verifying generics and delegates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 175\u2013199. Springer, Heidelberg (2010)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"van Staden, S., Calcagno, C.: Reasoning about multiple related abstractions with multistar. In: Proceedings of OOPSLA , pp. 504\u2013519 (2010)","DOI":"10.1145\/1869459.1869501"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/j.entcs.2008.10.022","volume":"218","author":"C. Varming","year":"2008","unstructured":"Varming, C., Birkedal, L.: Higher-order separation logic in Isabelle\/HOLCF. Electr. Notes Theor. Comput. Sci.\u00a0218, 371\u2013389 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T18:13:37Z","timestamp":1560449617000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}