{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:22:41Z","timestamp":1777519361587,"version":"3.51.4"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319712369","type":"print"},{"value":"9783319712376","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-71237-6_10","type":"book-chapter","created":{"date-parts":[[2017,11,17]],"date-time":"2017-11-17T20:13:02Z","timestamp":1510949582000},"page":"190-211","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Bringing Order to the Separation Logic Jungle"],"prefix":"10.1007","author":[{"given":"Qinxiang","family":"Cao","sequence":"first","affiliation":[]},{"given":"Santiago","family":"Cuellar","sequence":"additional","affiliation":[]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,19]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers, Cambridge (2014)","DOI":"10.1017\/CBO9781107256552"},{"issue":"5","key":"10_CR2","doi-asserted-by":"crossref","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"AW Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657\u2013683 (2001)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR3","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 the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2007)","DOI":"10.1145\/1190216.1190235"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. Logical Methods Comput. Sci. 7(2) (2011)","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"10_CR5","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. 6898, pp. 22\u201338. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_5"},{"key":"10_CR6","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 the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2011)","DOI":"10.1145\/1926385.1926401"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-28644-8_2","volume-title":"CONCUR 2004 - Concurrency Theory","author":"S Brookes","year":"2004","unstructured":"Brookes, S.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16\u201334. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-28644-8_2"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. In: 2010 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 130\u2013139. IEEE (2010)","DOI":"10.1109\/LICS.2010.24"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2014)","DOI":"10.1145\/2535838.2535844"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 366\u2013378, Washington, DC, USA. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash hoare logic for certifying the FSCQ file system. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, 4\u20137 October 2015, pp. 18\u201337. ACM (2015)","DOI":"10.1145\/2815400.2815402"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"10_CR13","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. 5904, pp. 161\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_13"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11944836_33","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"D Galmiche","year":"2006","unstructured":"Galmiche, D., Larchey-Wendling, D.: Expressivity properties of Boolean BI through relational models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 357\u2013368. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11944836_33"},{"issue":"6","key":"10_CR15","doi-asserted-by":"crossref","first-page":"1033","DOI":"10.1017\/S0960129505004858","volume":"15","author":"D Galmiche","year":"2005","unstructured":"Galmiche, D., M\u00e9ry, D., Pym, D.J.: The semantics of BI and resource tableaux. Mathe. Struct. Comput. Sci. 15(6), 1033\u20131088 (2005)","journal-title":"Mathe. Struct. Comput. Sci."},{"key":"10_CR16","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/j.entcs.2011.09.021","volume":"276","author":"A Gotsman","year":"2011","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Precision and the conjunction rule in concurrent separation logic. Electr. Notes Theor. Comput. Sci. 276, 171\u2013190 (2011)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Hobor, A., Dockins, R., Appel, A.W.: A theory of indirection via approximation. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2010)","DOI":"10.1145\/1706299.1706322"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Hur, C.-K., Dreyer, D., Vafeiadis, V.: Separation logic in the presence of garbage collection. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, 21\u201324 June 2011, Toronto, Ontario, Canada, pp. 247\u2013256 (2011)","DOI":"10.1109\/LICS.2011.46"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2001)","DOI":"10.1145\/360204.375719"},{"key":"10_CR20","unstructured":"Jensen, J.B.: Techniques for model construction in separation logic. Ph.D. thesis, IT University of Copenhagen, March 2014"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Jensen, J.B., Birkedal, L.: Fictional separation logic. In: Programming Languages and Systems - 21st European Symposium on Programming (2012)","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2015)","DOI":"10.1145\/2676726.2676980"},{"key":"10_CR23","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1016\/S0049-237X(08)71685-9","volume":"50","author":"SA Kripke","year":"1965","unstructured":"Kripke, S.A.: Semantical analysis of intuitionistic logic i. Studies Logic Found. Mathe. 50, 92\u2013130 (1965)","journal-title":"Studies Logic Found. Mathe."},{"issue":"3","key":"10_CR24","doi-asserted-by":"crossref","first-page":"435","DOI":"10.1017\/S0960129509007567","volume":"19","author":"D Larchey-Wendling","year":"2009","unstructured":"Larchey-Wendling, D., Galmiche, D.: Exploring the relation between intuitionistic BI and boolean BI: an unexpected embedding. Mathe. Struct. Comput. Sci. 19(3), 435\u2013500 (2009)","journal-title":"Mathe. Struct. Comput. Sci."},{"issue":"2","key":"10_CR25","doi-asserted-by":"crossref","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"PW O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symbolic Logic 5(2), 215\u2013244 (1999)","journal-title":"Bull. Symbolic Logic"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, 14\u201316 January 2004, pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-15057-9_12","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M Parkinson","year":"2010","unstructured":"Parkinson, M.: The next 700 separation logics. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 169\u2013182. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15057-9_12"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-642-19718-5_23","volume-title":"Programming Languages and Systems","author":"MJ Parkinson","year":"2011","unstructured":"Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 439\u2013458. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_23"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Pilkiewicz, A., Pottier, F.: The essence of monotonic state. In: Proceedings of TLDI 2011: 2011 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 73\u201386 (2011)","DOI":"10.1145\/1929553.1929565"},{"issue":"1","key":"10_CR30","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1017\/S0956796812000366","volume":"23","author":"F Pottier","year":"2013","unstructured":"Pottier, F.: Syntactic soundness proof of a type-and-capability system with hidden state. J. Funct. Program. 23(1), 38\u2013144 (2013)","journal-title":"J. Funct. Program."},{"issue":"1","key":"10_CR31","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/j.tcs.2003.11.020","volume":"315","author":"DJ Pym","year":"2004","unstructured":"Pym, D.J., O\u2019Hearn, P.W., Yang, H.: Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. 315(1), 257\u2013305 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR32","unstructured":"Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Millennial Perspectives in Computer Science, pp. 303\u2013321. Palgrave (2000)"},{"key":"10_CR33","unstructured":"Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic. Technical report, University of Edinburgh, College of Science and Engineering, School of Informatics (1994)"}],"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-319-71237-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T05:17:06Z","timestamp":1570339026000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-71237-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319712369","9783319712376"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-71237-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}