Iris: A Basis for Concurrent Reasoning
Iris is a higher-order impredicative concurrent separation logic with a simple premise: Ghost state and invariants are all you need. Resource algebras, a structured but generic form of ghost state, enable us to express — and invariants enable us to enforce — user-defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency.
The latest version of the technical development are available in the Git repository. This includes a Coq formalization of Iris, a rich body of examples, and a technical appendix covering the base logic and the program logic. The technical appendix is also available in compiled PDF form.
Discussion about Iris happens on the Iris-Club mailing list. This is also the right place to ask in case of trouble with the Coq formalization.
Higher-Order Ghost State
Ralf Jung, Robbert Krebbers, Lars Birkedal and Derek Dreyer
In ICFP 2016: ACM SIGPLAN International Conference on Functional Programming, Nara, Japan
[latest pdf] [technical appendix]
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer
In POPL 2015: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Mumbai, India
[latest pdf] [publisher's site] [technical appendix]
Original Coq formalizazion (now deprecated): [iris-20150616.zip] [README.txt] [older versions]