{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:05Z","timestamp":1774025825577,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370359","type":"print"},{"value":"9783642370366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37036-6_12","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:35:55Z","timestamp":1361216155000},"page":"189-208","source":"Crossref","is-referenced-by-count":6,"title":["Ribbon Proofs for Separation Logic"],"prefix":"10.1007","author":[{"given":"John","family":"Wickerson","sequence":"first","affiliation":[]},{"given":"Mike","family":"Dodds","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Parkinson","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Ashcroft, E.A.: Program verification tableaus. Technical Report CS-76-01, University of Waterloo (1976)"},{"key":"12_CR2","unstructured":"Bean, J.: Ribbon Proofs - A Proof System for the Logic of Bunched Implications. PhD thesis, Queen Mary University of London (2006)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL 2005. ACM Press (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., Yang, H.: Variables as resource in separation logic. In: MFPS XXI. ENTCS, vol.\u00a0155 (2006)","DOI":"10.1016\/j.entcs.2005.11.059"},{"key":"12_CR5","unstructured":"Bornat, R., Dodds, M.: Abducing barriers for Power and ARM. Draft (2012)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011. ACM Press (2011)","DOI":"10.1145\/1993498.1993526"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: Compositional reasoning for concurrent programs. In: POPL 2013. ACM Press (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T. Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent Abstract Predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 504\u2013528. Springer, Heidelberg (2010)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-642-00590-9_26","volume-title":"Programming Languages and Systems","author":"M. Dodds","year":"2009","unstructured":"Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-Guarantee Reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 363\u2013377. Springer, Heidelberg (2009)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL 2009. ACM Press (2009)","DOI":"10.1145\/1594834.1480922"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-71316-6_13","volume-title":"Programming Languages and Systems","author":"X. Feng","year":"2007","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 173\u2013188. Springer, Heidelberg (2007)"},{"key":"12_CR12","unstructured":"Fitch, F.B.: Symbolic Logic: An Introduction. Ronald Press Co. (1952)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50 (1987)","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-76637-7_3","volume-title":"Programming Languages and Systems","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local Reasoning for Storable Locks and Threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 19\u201337. Springer, Heidelberg (2007)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10) (1969)","DOI":"10.1145\/363235.363259"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Proof of a program: Find. Communications of the ACM 14(1) (1971)","DOI":"10.1145\/362452.362489"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Hur, C.-K., Dreyer, D., Vafeiadis, V.: Separation logic in the presence of garbage collection. In: LICS 2011. IEEE Computer Society (2011)","DOI":"10.1109\/LICS.2011.46"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL 2001. ACM Press (2001)","DOI":"10.1145\/360204.375719"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-642-21437-0_30","volume-title":"FM 2011: Formal Methods","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Piessens, F.: Verification of Unloadable Modules. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 402\u2013416. Springer, Heidelberg (2011)"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Joyal, A., Street, R., Verity, D.: Traced monoidal categories. Math. Proc. of the Cambridge Philosophical Society 119(3) (1996)","DOI":"10.1017\/S0305004100074338"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Milner, R.: The Space and Motion of Communicating Agents. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511626661"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comput. Sci. 375(1-3) (2007)","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. B. Symb. Log. 5(2) (1999)","DOI":"10.2307\/421090"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6 (1976)","DOI":"10.1007\/BF00268134"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-00590-9_25","volume-title":"Programming Languages and Systems","author":"M. Raza","year":"2009","unstructured":"Raza, M., Calcagno, C., Gardner, P.: Automatic Parallelization with Separation Logic. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 348\u2013362. Springer, Heidelberg (2009)"},{"key":"12_CR27","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002. IEEE Computer Society (2002)"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Schneider, F.B.: On Concurrent Programming, ch. 4. Springer (1997)","DOI":"10.1007\/978-1-4612-1830-2"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Selinger, P.: A survey of graphical languages for monoidal categories. In: New Structures for Physics, vol.\u00a0813, ch. 4. Springer (2011)","DOI":"10.1007\/978-3-642-12821-9_4"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-642-31365-3_44","volume-title":"Automated Reasoning","author":"M. Urbas","year":"2012","unstructured":"Urbas, M., Jamnik, M.: Diabelli: A Heterogeneous Proof System. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 559\u2013566. Springer, Heidelberg (2012)"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A Marriage of Rely\/Guarantee and Separation Logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"12_CR32","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Asynchronous proof processing with Isabelle\/Scala and Isabelle\/jEdit. In: UITP 2010. ENTCS, vol.\u00a0285 (2012)","DOI":"10.1016\/j.entcs.2012.06.009"},{"key":"12_CR33","unstructured":"Wickerson, J.: Concurrent Verification for Sequential Programs. PhD thesis, University of Cambridge (2013)"},{"key":"12_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-642-22863-6_25","volume-title":"Interactive Theorem Proving","author":"C. Wu","year":"2011","unstructured":"Wu, C., Zhang, X., Urban, C.: A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl). In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 341\u2013356. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37036-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,8]],"date-time":"2022-02-08T22:07:46Z","timestamp":1644358066000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}