{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:47:41Z","timestamp":1770281261569,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642390371","type":"print"},{"value":"9783642390388","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39038-8_14","type":"book-chapter","created":{"date-parts":[[2013,6,25]],"date-time":"2013-06-25T10:29:00Z","timestamp":1372156140000},"page":"327-351","source":"Crossref","is-referenced-by-count":5,"title":["Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library"],"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":"14_CR1","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":"14_CR2","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Proceedings of POPL, pp. 259\u2013270 (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"issue":"10","key":"14_CR4","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1145\/362759.362813","volume":"14","author":"P.-J. Courtois","year":"1971","unstructured":"Courtois, P.-J., Heymans, F., Parnas, D.L.: Concurrent Control with \u201cReaders\u201d and \u201cWriters\u201d. Commun. ACM\u00a014(10), 667\u2013668 (1971)","journal-title":"Commun. ACM"},{"issue":"10","key":"14_CR5","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1145\/2076021.2048131","volume":"46","author":"P. Rocha Pinto da","year":"2011","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Dodds, M., Gardner, P., Wheelhouse, M.: A simple abstraction for complex concurrent indexes. SIGPLAN Not.\u00a046(10), 845\u2013864 (2011)","journal-title":"SIGPLAN Not."},{"key":"14_CR6","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":"14_CR7","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":"14_CR8","unstructured":"Fournet, C., Gonthier, G.: The reflexive chemical abstract machine and the join-calculus. In: Proceedings of POPL (1996)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-45699-6_6","volume-title":"Applied Semantics","author":"C. Fournet","year":"2002","unstructured":"Fournet, C., Gonthier, G.: The Join Calculus: A Language for Distributed Mobile Programming. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol.\u00a02395, pp. 268\u2013332. Springer, Heidelberg (2002)"},{"key":"14_CR10","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":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-78739-6_27","volume-title":"Programming Languages and Systems","author":"A. Hobor","year":"2008","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle Semantics for Concurrent Separation Logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 353\u2013367. Springer, Heidelberg (2008)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-642-19718-5_15","volume-title":"Programming Languages and Systems","author":"A. Hobor","year":"2011","unstructured":"Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 276\u2013296. Springer, Heidelberg (2011)"},{"key":"14_CR13","unstructured":"Jacobs, B.: Verified general barriers implementation, \n                    \n                      http:\/\/people.cs.kuleuven.be\/~bart.jacobs\/verifast\/examples\/barrier.c.html"},{"key":"14_CR14","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":"14_CR15","unstructured":"Krishnaswami, N.: Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. PhD thesis, Carnegie Mellon University (2012)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N., Birkedal, L., Aldrich, J.: Verifying Event-Driven Programs using Ramified Frame Properties. In: Proceedings of TLDI (2010)","DOI":"10.1145\/1708016.1708025"},{"issue":"1-3","key":"14_CR17","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, Concurrency and Local Reasoning. Theor. Comput. Sci.\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"14_CR18","unstructured":"Owicki, S.S.: Axiomatic Proof Techniques for Parallel Programs. PhD thesis, Cornell (1975)"},{"key":"14_CR19","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\/1047659.1040326"},{"key":"14_CR20","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":"14_CR21","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":"14_CR22","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":"14_CR23","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":"14_CR24","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Verification of the Joins Library in Higher-order Separation Logic. Technical report, IT University of Copenhagen (2012), \n                    \n                      http:\/\/www.itu.dk\/people\/kasv\/joins-tr.pdf"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Impredicative Concurrent Abstract Predicates. Under submission (2013)","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/978-3-642-37036-6_11","volume-title":"ESOP 2013","author":"K. Svendsen","year":"2013","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Modular Reasoning about Separation of Concurrent Data Structures. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 169\u2013188. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2013 \u2013 Object-Oriented Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39038-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:38:12Z","timestamp":1558301892000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39038-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642390371","9783642390388"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39038-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}