{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T12:03:40Z","timestamp":1763726620388,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642323461"},{"type":"electronic","value":"9783642323478"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_21","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T11:33:54Z","timestamp":1344598434000},"page":"315-331","source":"Crossref","is-referenced-by-count":19,"title":["Charge!"],"prefix":"10.1007","author":[{"given":"Jesper","family":"Bengtson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonas Braband","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"Appel, A.W.: Tactics for separation logic, Draft (January 2006), http:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-22863-6_5","volume-title":"Interactive Theorem Proving","author":"J. Bengtson","year":"2011","unstructured":"Bengtson, J., Jensen, J.B., Sieczkowski, F., Birkedal, L.: Verifying Object-Oriented Programs with Higher-Order Separation Logic in COQ. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 22\u201338. Springer, Heidelberg (2011)"},{"key":"21_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":"21_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":"21_CR5","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":"21_CR6","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI, pp. 234\u2013245 (2011)","DOI":"10.1145\/1993316.1993526"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-10672-9_13","volume-title":"Programming Languages and Systems","author":"R. Dockins","year":"2009","unstructured":"Dockins, R., Hobor, A., Appel, A.W.: A Fresh Look at Separation Algebras and Share Accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 161\u2013177. Springer, Heidelberg (2009)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Dodds, M., Jagannathan, S., Parkinson, M.J.: Modular reasoning for deterministic parallelism. In: Proceedings of POPL (2011)","DOI":"10.1145\/1926385.1926416"},{"key":"21_CR9","unstructured":"Jacobs, B., Piessens, F.: The verifast program verifier. CW Reports CW520, Department of Computer Science, K.U. Leuven (August 2008)"},{"key":"21_CR10","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":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-03359-9_24","volume-title":"Theorem Proving in Higher Order Logics","author":"A. McCreight","year":"2009","unstructured":"McCreight, A.: Practical Tactics for Separation Logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 343\u2013358. Springer, Heidelberg (2009)"},{"key":"21_CR12","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":"21_CR13","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bornat, R., Calcagno, C.: Variables as resource in Hoare logic. In: Proceedings of LICS, pp. 137\u2013146. IEEE (2006)","DOI":"10.1109\/LICS.2006.52"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-04027-6_32","volume-title":"Computer Science Logic","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":"21_CR15","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":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-642-03359-9_32","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Tuerk","year":"2009","unstructured":"Tuerk, T.: A Formalisation of Smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 469\u2013484. Springer, Heidelberg (2009)"},{"key":"21_CR17","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-32347-8_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,6]],"date-time":"2025-04-06T19:25:41Z","timestamp":1743967541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}