Congratulations to Jacques-Henri Jourdan and his co-authors who will receive the 2023 Alonzo Church Award for their outstanding contributions to Logic and computation with the design and implementation of Iris, a higher-order concurrent separation logic framework. The Award will be presented at the 50th EATCS International Colloquium on Automata, Languages and Programming, ICALP 2023, in July.
Iris has been widely used in academia, and also in industry, e.g., by engineers at Meta to verify the core components of an interprocess communication system for a new operating system.
- Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer: “Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning”. POPL 2015.
- Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer: “Higher-order ghost state”. ICFP 2016.
- Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal: “The Essence of Higher-Order Concurrent Separation Logic”. ESOP 2017.
- Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, Derek Dreyer: “Iris from the ground up: A modular foundation for higher-order concurrent separation logic”. J. Funct. Program. 28 (2018).
For more information about Iris, see iris-project.org