{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:06Z","timestamp":1775873406106,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642548321","type":"print"},{"value":"9783642548338","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54833-8_9","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T05:37:17Z","timestamp":1395380237000},"page":"149-168","source":"Crossref","is-referenced-by-count":99,"title":["Impredicative Concurrent Abstract Predicates"],"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"}]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Node.js, \n                    \n                      http:\/\/www.nodejs.org"},{"key":"9_CR2","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 POPL (2007)","DOI":"10.1145\/1190216.1190235"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-32347-8_21","volume-title":"Interactive Theorem Proving","author":"J. Bengtson","year":"2012","unstructured":"Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 315\u2013331. Springer, Heidelberg (2012)"},{"key":"9_CR4","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: Proceedings of LICS (2011)","DOI":"10.1109\/LICS.2011.16"},{"key":"9_CR5","unstructured":"Birkedal, L., Sieczkowski, F., Thamsborg, J.: A Concurrent Logical Relation. In: Proceedings of CSL (2012)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic. In: Proceedings of PLDI (2011)","DOI":"10.1145\/1993498.1993526"},{"key":"9_CR7","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":"9_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":"9_CR9","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":"9_CR10","doi-asserted-by":"crossref","unstructured":"Dreyer, D., Neis, G., Birkedal, L.: The Impact of Higher-Order State and Control Effects on Local Relational Reasoning. In: Proceedings of ICFP (2010)","DOI":"10.1145\/1863543.1863566"},{"key":"9_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":"9_CR12","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":"9_CR13","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (2008)"},{"key":"9_CR14","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":"9_CR15","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: POPL (2012)","DOI":"10.1145\/2103656.2103711"},{"issue":"1-3","key":"9_CR16","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":"9_CR17","unstructured":"Owicki, S.S.: Axiomatic Proof Techniques for Parallel Programs. PhD thesis, Cornell (1975)"},{"key":"9_CR18","unstructured":"Provos, N., Mathewson, N.: libevent \u2013 an event notification library, \n                    \n                      http:\/\/www.monkey.org\/~provos\/libevent"},{"key":"9_CR19","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":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-39038-8_14","volume-title":"ECOOP 2013 \u2013 Object-Oriented Programming","author":"K. Svendsen","year":"2013","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Joins: a Case Study in Modular Specification of a Concurrent Reentrant Higher-order Library. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol.\u00a07920, pp. 327\u2013351. Springer, Heidelberg (2013)"},{"key":"9_CR21","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying Refinement and Hoare-Style Reasoning in a Logic for Higher-Order Concurrency. In: Proceedings of ICFP (2013)","DOI":"10.1145\/2500365.2500600"},{"key":"9_CR23","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"},{"key":"9_CR24","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)"}],"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-54833-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T08:27:31Z","timestamp":1558859251000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54833-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548321","9783642548338"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}