{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:27Z","timestamp":1781238927460,"version":"3.54.1"},"reference-count":76,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2018,11,22]],"date-time":"2018-11-22T00:00:00Z","timestamp":1542844800000},"content-version":"unspecified","delay-in-days":325,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2018]]},"abstract":"<jats:p>\n                    <jats:bold>Iris<\/jats:bold>\n                    is a framework for higher-order concurrent separation logic, which has been implemented in the Coq proof assistant and deployed very effectively in a wide variety of verification projects. Iris was designed with the express goal of simplifying and consolidating the foundations of modern separation logics, but it has evolved over time, and the design and semantic foundations of Iris itself have yet to be fully written down and explained together properly in one place. Here, we attempt to fill this gap, presenting a reasonably complete picture of the latest version of Iris (version 3.1), from first principles and in one coherent narrative.\n                  <\/jats:p>","DOI":"10.1017\/s0956796818000151","type":"journal-article","created":{"date-parts":[[2018,11,22]],"date-time":"2018-11-22T04:13:14Z","timestamp":1542859994000},"source":"Crossref","is-referenced-by-count":298,"title":["Iris from the ground up: A modular foundation for higher-order concurrent separation logic"],"prefix":"10.1017","volume":"28","author":[{"given":"RALF","family":"JUNG","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ROBBERT","family":"KREBBERS","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"JACQUES-HENRI","family":"JOURDAN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ALE\u0160","family":"BIZJAK","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"LARS","family":"BIRKEDAL","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DEREK","family":"DREYER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2018,11,22]]},"reference":[{"key":"S0956796818000151_ref75","unstructured":"Vafeiadis, Viktor , & Parkinson, Matthew J. (2007). A marriage of rely\/guarantee and separation logic. Pages 256\u2013271 of: CONCUR. LNCS, vol. 4703."},{"key":"S0956796818000151_ref72","first-page":"64:1","article-title":"A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST","volume":"2","author":"Timany","year":"2018","journal-title":"PACMPL"},{"key":"S0956796818000151_ref71","unstructured":"Timany, Amin , & Birkedal, Lars . (2018). Mechanized relational verification of concurrent programs with continuations. Draft."},{"key":"S0956796818000151_ref70","unstructured":"Tassarotti, Joseph , Jung, Ralf , & Harper, Robert . (2017). A higher-order logic for concurrent termination-preserving refinement. Pages 909\u2013936 of: ESOP. LNCS, vol. 10201."},{"key":"S0956796818000151_ref68","first-page":"89:1","article-title":"Robust and compositional verification of object capability patterns","volume":"1","author":"Swasey","year":"2017","journal-title":"PACMPL"},{"key":"S0956796818000151_ref64","unstructured":"Reynolds, John C. (2002). Separation logic: A logic for shared mutable data structures. Pages 55\u201374 of: LICS."},{"key":"S0956796818000151_ref61","unstructured":"Pilkiewicz, Alexandre , & Pottier, Fran\u00e7ois . (2011). The essence of monotonic state. Pages 73\u201386 of: TLDI."},{"key":"S0956796818000151_ref65","unstructured":"Sergey, Ilya , Nanevski, Aleksandar , & Banerjee, Anindya . (2015). Mechanized verification of fine-grained concurrent programs. Pages 77\u201387 of: PLDI."},{"key":"S0956796818000151_ref60","unstructured":"Parkinson, Matthew J. (2010). The next 700 separation logics - (Invited paper). Pages 169\u2013182 of: VSTTE. LNCS, vol. 6217."},{"key":"S0956796818000151_ref57","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"S0956796818000151_ref55","unstructured":"Nakano, Hiroshi . (2000). A modality for recursion. Pages 255\u2013266 of: LICS."},{"key":"S0956796818000151_ref53","unstructured":"Ley-Wild, Ruy , & Nanevski, Aleksandar . (2013). Subjective auxiliary state for coarse-grained concurrency. Pages 561\u2013574 of: POPL."},{"key":"S0956796818000151_ref52","unstructured":"Leino, K. Rustan, M. , M\u00fcller, Peter , & Smans, Jan . (2009). Verification of concurrent programs with Chalice. Pages 195\u2013222 of: FOSAD. LNCS, vol. 5705."},{"key":"S0956796818000151_ref51","unstructured":"Leino, K. Rustan, M. (2010). Dafny: An automatic program verifier for functional correctness. Pages 348\u2013370 of: LPAR. LNCS, vol. 6355."},{"key":"S0956796818000151_ref49","unstructured":"Krishnaswami, Neelakantan R. , Turon, Aaron , Dreyer, Derek , & Garg, Deepak . (2012). Superficially substructural types. Pages 41\u201354 of: ICFP."},{"key":"S0956796818000151_ref69","unstructured":"Tassarotti, Joseph , & Harper, Robert . (2018). A separation logic for concurrent randomized programs. Draft."},{"key":"S0956796818000151_ref66","first-page":"41","article-title":"A new look at generalized rewriting in type theory","volume":"2","author":"Sozeau","year":"2009","journal-title":"Journal of formalized reasoning"},{"key":"S0956796818000151_ref47","first-page":"77:1","article-title":"MoSeL: A general, extensible modal framework for interactive proofs in separation logic","volume":"2","author":"Krebbers","year":"2018","journal-title":"PACMPL"},{"key":"S0956796818000151_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"S0956796818000151_ref12","unstructured":"Bornat, Richard , Calcagno, Cristiano , O\u2019Hearn, Peter W. , & Parkinson, Matthew J. (2005). Permission accounting in separation logic. Pages 259\u2013270 of: POPL."},{"key":"S0956796818000151_ref58","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"S0956796818000151_ref2","unstructured":"Appel, Andrew W. (2001). Foundational proof-carrying code. Pages 247\u2013256 of: LICS."},{"key":"S0956796818000151_ref15","first-page":"121","article-title":"Step-indexed Kripke model of separation logic for storable locks","volume":"276","author":"Buisse","year":"2011","journal-title":"ENTCS"},{"key":"S0956796818000151_ref62","first-page":"38","article-title":"Syntactic soundness proof of a type-and-capability system with hidden state","volume":"23","author":"Pottier","year":"2013","journal-title":"JFP"},{"key":"S0956796818000151_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"S0956796818000151_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"S0956796818000151_ref11","unstructured":"Bizjak, Ale\u0161 , Gratzer, Daniel , Krebbers, Robbert , & Birkedal, Lars . (2018). Iron: Managing obligations in higher-order concurrent separation logic. Draft."},{"key":"S0956796818000151_ref25","unstructured":"Dodds, Mike , Feng, Xinyu , Parkinson, Matthew J. , & Vafeiadis, Viktor . (2009). Deny-guarantee reasoning. Pages 363\u2013377 of: ESOP. LNCS, vol. 5502."},{"key":"S0956796818000151_ref34","unstructured":"Hobor, Aquinas , Appel, Andrew W. , & Zappa Nardelli, Francesco . (2008). Oracle semantics for concurrent separation logic. Pages 353\u2013367 of: ESOP. LNCS, vol. 4960."},{"key":"S0956796818000151_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"S0956796818000151_ref39","unstructured":"Jung, Ralf , Swasey, David , Sieczkowski, Filip , Svendsen, Kasper , Turon, Aaron , Birkedal, Lars , & Dreyer, Derek . (2015). Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. Pages 637\u2013650 of: POPL."},{"key":"S0956796818000151_ref31","unstructured":"Fu, Ming , Li, Yong , Feng, Xinyu , Shao, Zhong , & Zhang, Yu . (2010). Reasoning about optimistic concurrency using a program logic for history. Pages 388\u2013402 of: CONCUR. LNCS, vol. 6269."},{"key":"S0956796818000151_ref17","unstructured":"Cohen, Ernie , Alkassar, Eyad , Boyarinov, Vladimir , Dahlweid, Markus , Degenbaev, Ulan , Hillebrand, Mark , Langenstein, Bruno , Leinenbach, Dirk , Moskal, Micha\u0142 , Obua, Steven , Paul, Wolfgang , Pentchev, Hristo , Petrova, Elena , Santen, Thomas , Schirmer, Norbert , Schmaltz, Sabine , Schulte, Wolfram , Shadrin, Andrey , Tobies, Stephan , Tsyban, Alexandra , & Tverdyshev, Sergey . (2009). Invariants, modularity, and rights. Pages 43\u201355 of: PSI. LNCS, vol. 5947."},{"key":"S0956796818000151_ref73","unstructured":"Turon, Aaron , Dreyer, Derek , & Birkedal, Lars . (2013). Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. Pages 377\u2013390 of: ICFP."},{"key":"S0956796818000151_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"S0956796818000151_ref32","unstructured":"Garillot, Fran\u00e7ois , Gonthier, Georges , Mahboubi, Assia , & Rideau, Laurence . (2009). Packaging mathematical structures. Pages 327\u2013342 of: TPHOLs. LNCS, vol. 5674."},{"key":"S0956796818000151_ref54","unstructured":"M\u00fcller, Peter , Schwerhoff, Malte , & Summers, Alexander J. (2016). Viper: A verification infrastructure for permission-based reasoning. Pages 41\u201362 of: VMCAI. LNCS, vol. 9583."},{"key":"S0956796818000151_ref18","unstructured":"da Rocha Pinto, Pedro , Dinsdale-Young, Thomas , & Gardner, Philippa . (2014). TaDA: A logic for time and data abstraction. Pages 207\u2013231 of: ECOOP. LNCS, vol. 8586."},{"key":"S0956796818000151_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80018-3"},{"key":"S0956796818000151_ref13","unstructured":"Boyland, John . (2003). Checking interference with fractional permissions. Pages 55\u201372 of: SAS. LNCS, vol. 2694."},{"key":"S0956796818000151_ref9","unstructured":"Birkedal, Lars , M\u00f8gelberg, Rasmus Ejlers , Schwinghammer, Jan , & St\u00f8vring, Kristian . (2011). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Pages 55\u201364 of: LICS."},{"key":"S0956796818000151_ref5","unstructured":"Appel, Andrew W. , Melli\u00e8s, Paul-Andr\u00e9 , Richards, Christopher , & Vouillon, J\u00e9r\u00f4me . (2007). A very modal model of a modern, major, general type system. Pages 109\u2013122 of: POPL."},{"key":"S0956796818000151_ref7","unstructured":"Beringer, Lennart , Stewart, Gordon , Dockins, Robert , & Appel, Andrew W. (2014). Verified compilation for shared-memory C. Pages 107\u2013127 of: ESOP. LNCS, vol. 8410."},{"key":"S0956796818000151_ref50","unstructured":"Krogh-Jespersen, Morten , Svendsen, Kasper , & Birkedal, Lars . (2017). A relational model of types-and-effects in higher-order concurrent separation logic. Pages 218\u2013231 of: POPL."},{"key":"S0956796818000151_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_14"},{"key":"S0956796818000151_ref16","unstructured":"Cao, Qinxiang , Cuellar, Santiago , & Appel, Andrew W. (2017). Bringing order to the separation logic jungle. Pages 190\u2013211 of: APLAS. LNCS, vol. 10695."},{"key":"S0956796818000151_ref33","unstructured":"Gotsman, Alexey , Berdine, Josh , Cook, Byron , Rinetzky, Noam , & Sagiv, Mooly . (2007). Local reasoning about storable locks and threads. Pages 19\u201337 of: APLAS. LNCS, vol. 4807."},{"key":"S0956796818000151_ref74","unstructured":"Turon, Aaron , Vafeiadis, Viktor , & Dreyer, Derek . (2014). GPS: Navigating weak memory with ghosts, protocols, and separation. Pages 691\u2013707 of: OOPSLA."},{"key":"S0956796818000151_ref56","unstructured":"Nanevski, Aleksandar , Ley-Wild, Ruy , Sergey, Ilya , & Delbianco, Germ\u00e1n Andr\u00e9s . (2014). Communicating state transition systems for fine-grained concurrent resources. Pages 290\u2013310 of: ESOP. LNCS, vol. 8410."},{"key":"S0956796818000151_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/BF01304852"},{"key":"S0956796818000151_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"S0956796818000151_ref67","unstructured":"Svendsen, Kasper , & Birkedal, Lars . (2014). Impredicative concurrent abstract predicates. Pages 149\u2013168 of: ESOP. LNCS, vol. 8410."},{"key":"S0956796818000151_ref19","unstructured":"Di Gianantonio, Pietro , & Miculan, Marino . (2002). A unifying approach to recursive and co-recursive definitions. Pages 148\u2013161 of: TYPES. LNCS, vol. 2646."},{"key":"S0956796818000151_ref10","unstructured":"Bizjak, Ale\u0161 , & Birkedal, Lars . (2017). On models of higher-order separation logic. MFPS."},{"key":"S0956796818000151_ref63","unstructured":"Reynolds, John C. (2000). Intuitionistic reasoning about shared mutable data structure. Pages 303\u2013321 of: Millennial Perspectives in Computer Science."},{"key":"S0956796818000151_ref24","unstructured":"Dockins, Robert , Hobor, Aquinas , & Appel, Andrew W. (2009). A fresh look at separation algebras and share accounting. Pages 161\u2013177 of: APLAS. LNCS, vol. 5904."},{"key":"S0956796818000151_ref27","unstructured":"Dreyer, Derek , Neis, Georg , Rossberg, Andreas , & Birkedal, Lars . (2010). A relational modal logic for higher-order stateful ADTs. Pages 185\u2013198 of: POPL."},{"key":"S0956796818000151_ref28","unstructured":"Feng, Xinyu . (2009). Local rely-guarantee reasoning. Pages 315\u2013327 of: POPL."},{"key":"S0956796818000151_ref23","unstructured":"Dinsdale-Young, Thomas , Birkedal, Lars , Gardner, Philippa , Parkinson, Matthew J. , & Yang, Hongseok . (2013). Views: Compositional reasoning for concurrent programs. Pages 287\u2013300 of: POPL."},{"key":"S0956796818000151_ref29","unstructured":"Feng, Xinyu , Ferreira, Rodrigo , & Shao, Zhong . (2007). On the relationship between concurrent separation logic and assume-guarantee reasoning. Pages 173\u2013188 of: ESOP. LNCS, vol. 4421."},{"key":"S0956796818000151_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"S0956796818000151_ref30","unstructured":"Frumin, Dan , Krebbers, Robbert , & Birkedal, Lars . (2018). ReLoC: A mechanised relational logic for fine-grained concurrency. Pages 442\u2013451 of: LICS."},{"key":"S0956796818000151_ref35","unstructured":"Hobor, Aquinas , Dockins, Robert , & Appel, Andrew W. (2010). A theory of indirection via approximation. Pages 171\u2013184 of: POPL."},{"key":"S0956796818000151_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"S0956796818000151_ref36","unstructured":"Iris Team. (2017). The Iris documentation and Coq development. Available on the Iris project website at: http:\/\/iris-project.org."},{"key":"S0956796818000151_ref38","unstructured":"Jensen, Jonas Braband , & Birkedal, Lars . (2012). Fictional separation logic. Pages 377\u2013396 of: ESOP. LNCS, vol. 7211."},{"key":"S0956796818000151_ref37","unstructured":"Ishtiaq, Samin S. , & O\u2019Hearn, Peter W. (2001). BI as an assertion language for mutable data structures. Pages 14\u201326 of: POPL."},{"key":"S0956796818000151_ref40","unstructured":"Jung, Ralf , Krebbers, Robbert , Birkedal, Lars , & Dreyer, Derek . (2016). Higher-order ghost state. Pages 256\u2013269 of: ICFP."},{"key":"S0956796818000151_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2818638"},{"key":"S0956796818000151_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009855"},{"key":"S0956796818000151_ref76","unstructured":"Wildmoser, Martin , & Nipkow, Tobias . (2004). Certifying machine code safety: Shallow versus deep embedding. Pages 305\u2013320 of: TPHOLs. LNCS, vol. 3223."},{"key":"S0956796818000151_ref41","first-page":"66:1","article-title":"RustBelt: Securing the foundations of the Rust programming language","volume":"2","author":"Jung","year":"2018","journal-title":"PACMPL"},{"key":"S0956796818000151_ref42","unstructured":"Kaiser, Jan-Oliver , Dang, Hoang-Hai , Dreyer, Derek , Lahav, Ori , & Vafeiadis, Viktor . (2017). Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. Pages 17:1\u201317:29 of: ECOOP. LIPIcs, vol. 74."},{"key":"S0956796818000151_ref59","unstructured":"O\u2019Hearn, Peter W. , Reynolds, John C. , & Yang, Hongseok . (2001). Local reasoning about programs that alter data structures. Pages 1\u201318 of: CSL. LNCS, vol. 2142."},{"key":"S0956796818000151_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/BF01220868"},{"key":"S0956796818000151_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796818000151","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:47Z","timestamp":1779835007000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796818000151\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"references-count":76,"alternative-id":["S0956796818000151"],"URL":"https:\/\/doi.org\/10.1017\/s0956796818000151","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"article-number":"e20"}}