{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:07:40Z","timestamp":1774987660517,"version":"3.50.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319221014","type":"print"},{"value":"9783319221021","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_25","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T08:30:14Z","timestamp":1439886614000},"page":"375-390","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages"],"prefix":"10.1007","author":[{"given":"Filip","family":"Sieczkowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ale\u0161","family":"Bizjak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"key":"25_CR1","unstructured":"Ahmed, A.: Semantics of Types for Mutable State. Ph.D. thesis, Princeton University (2004)"},{"key":"25_CR2","unstructured":"Ahmed, A., Appel, A.W., Virga, R.: A stratified semantics of general references embeddable in higher-order logic. In: LICS (2002)"},{"key":"25_CR3","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: POPL (2007)","DOI":"10.1145\/1190216.1190235"},{"key":"25_CR4","unstructured":"Appel, A.W., Dockins, R., Hobor, A.: (2009). http:\/\/vst.cs.princeton.edu\/msl\/"},{"key":"25_CR5","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! - a framework for higher-order separation logic in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 315\u2013331. Springer, Heidelberg (2012)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-03359-9_10","volume-title":"Theorem Proving in Higher Order Logics","author":"N Benton","year":"2009","unstructured":"Benton, N., Kennedy, A., Varming, C.: Some domain theory and denotational semantics in Coq. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 115\u2013130. Springer, Heidelberg (2009)"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-31987-0_17","volume-title":"Programming Languages and Systems","author":"B Biering","year":"2005","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI hyperdoctrines and higher-order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 233\u2013247. Springer, Heidelberg (2005)"},{"key":"25_CR8","unstructured":"Birkedal, L., Bizjak, A.: A taste of categorical logic - tutorial notes (2014). http:\/\/cs.au.dk\/~birke\/modures\/tutorial\/categorical-logic-tutorial-notes.pdf"},{"key":"25_CR9","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: POPL (2011)","DOI":"10.1145\/1926385.1926401"},{"issue":"47","key":"25_CR10","doi-asserted-by":"publisher","first-page":"4102","DOI":"10.1016\/j.tcs.2010.07.010","volume":"411","author":"L Birkedal","year":"2010","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: The category-theoretic solution of recursive metric-space equations. Theor. Comput. Sci. 411(47), 4102\u20134122 (2010)","journal-title":"Theor. Comput. Sci."},{"key":"25_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-00596-1_32","volume-title":"Foundations of Software Science and Computational Structures","author":"L Birkedal","year":"2009","unstructured":"Birkedal, L., St\u00f8vring, K., Thamsborg, J.: Realizability semantics of parametric polymorphism, general references, and recursive types. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 456\u2013470. Springer, Heidelberg (2009)"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: POPL (2014)","DOI":"10.1145\/2535838.2535844"},{"key":"25_CR13","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. In: ICFP (2013)","DOI":"10.1145\/2500365.2500592"},{"key":"25_CR15","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)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-39185-1_9","volume-title":"Types for Proofs and Programs","author":"P Di Gianantonio","year":"2003","unstructured":"Di Gianantonio, P., Miculan, M.: A unifying approach to recursive and co-recursive definitions. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 148\u2013161. Springer, Heidelberg (2003)"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Hobor, A., Dockins, R., Appel, A.: A theory of indirection via approximation. In: POPL (2010)","DOI":"10.1145\/1706299.1706322"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-03359-9_19","volume-title":"Theorem Proving in Higher Order Logics","author":"B Huffman","year":"2009","unstructured":"Huffman, B.: A purely definitional universal domain. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 260\u2013275. Springer, Heidelberg (2009)"},{"key":"25_CR19","unstructured":"Jensen, J.B.: Enabling Concise and Modular Specifications in Separation Logic. Ph.D. thesis, IT University of Copenhagen (2014)"},{"key":"25_CR20","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: POPL (2015)","DOI":"10.1145\/2676726.2676980"},{"key":"25_CR21","unstructured":"Malecha, G., Bengtson, J.: Rtac \u2013 a reflective tactic language for Coq (2015) (Submitted for publication)"},{"issue":"1","key":"25_CR22","first-page":"38","volume":"23","author":"F Pottier","year":"2013","unstructured":"Pottier, F.: Syntactic soundness proof of a type-and-capability system with hidden state. JFP 23(1), 38\u2013144 (2013)","journal-title":"JFP"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"issue":"4","key":"25_CR24","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795\u2013825 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"K Svendsen","year":"2014","unstructured":"Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 149\u2013168. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,16]],"date-time":"2023-02-16T21:56:06Z","timestamp":1676584566000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}