{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:39Z","timestamp":1775873679195,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"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_11","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:35:55Z","timestamp":1361216155000},"page":"169-188","source":"Crossref","is-referenced-by-count":41,"title":["Modular Reasoning about Separation of Concurrent Data Structures"],"prefix":"10.1007","author":[{"given":"Kasper","family":"Svendsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Parkinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A., Melli\u00e8s, P.-A., Richards, C., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proc. of POPL (2007)","DOI":"10.1145\/1190216.1190235"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI-Hyperdoctrines, Higher-order Separation Logic, and Abstraction. ACM TOPLAS (2007)","DOI":"10.1145\/1275497.1275499"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, R., Schwinghammer, J., St\u00f8vring, K.: First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. In: Proc. of LICS (2011)","DOI":"10.1109\/LICS.2011.16"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: Compositional Reasoning for Concurrent Programs. In: Proceedings of POPL (2013)","DOI":"10.1145\/2429069.2429104"},{"key":"11_CR5","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":"11_CR6","doi-asserted-by":"crossref","unstructured":"Dodds, M., Jagannathan, S., Parkinson, M.J.: Modular reasoning for deterministic parallelism. In: Proceedings of POPL, pp. 259\u2013270 (2011)","DOI":"10.1145\/1925844.1926416"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-00590-9_19","volume-title":"Programming Languages and Systems","author":"I. Filipovi\u0107","year":"2009","unstructured":"Filipovi\u0107, I., O\u2019Hearn, P., Rinetzky, N., Yang, H.: Abstraction for Concurrent Objects. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 252\u2013266. Springer, Heidelberg (2009)"},{"key":"11_CR8","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (2008)"},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M.P. Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM TOPLAS\u00a012, 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: Proceedings of POPL, pp. 271\u2013282 (2011)","DOI":"10.1145\/1925844.1926417"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-28869-2_19","volume-title":"Programming Languages and Systems","author":"J.B. Jensen","year":"2012","unstructured":"Jensen, J.B., Birkedal, L.: Fictional Separation Logic. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 377\u2013396. Springer, Heidelberg (2012)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Lea, D.: A java fork\/join framework. In: Proceedings of the ACM 2000 Conference on Java Grande, JAVA 2000, pp. 36\u201343. ACM (2000)","DOI":"10.1145\/337449.337465"},{"key":"11_CR13","unstructured":"Owicki, S.S.: Axiomatic Proof Techniques for Parallel Programs. PhD thesis, Cornell (1975)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bornat, R., O\u2019Hearn, P.: Modular verification of a non-blocking stack. SIGPLAN Not. 42(1) (2007)","DOI":"10.1145\/1190215.1190261"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Pilkiewicz, A., Pottier, F.: The essence of monotonic state. In: Proceedings of TLDI, pp. 73\u201386 (2011)","DOI":"10.1145\/1929553.1929565"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-69611-7_17","volume-title":"Practical Aspects of Declarative Languages","author":"C.V. Russo","year":"2007","unstructured":"Russo, C.V.: The Joins Concurrency Library. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 260\u2013274. Springer, Heidelberg (2007)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare Triples and Frame Rules for Higher-Order Store. LMCS 7(3:21) (2011)","DOI":"10.2168\/LMCS-7(3:21)2011"},{"key":"11_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":"11_CR19","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Higher-order Concurrent Abstract Predicates. Technical report, IT University of Copenhagen (2012), \n                    \n                      http:\/\/www.itu.dk\/people\/kasv\/hocap-tr.pdf"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Turon, A., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical Relations for Fine-Grained Concurrency. In: Proceedings of POPL (2013)","DOI":"10.1145\/2429069.2429111"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,11]],"date-time":"2019-05-11T08:43:35Z","timestamp":1557564215000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}