Iris is a higher-order concurrent separation logic framework, implemented and verified in the Coq proof assistant. This means that Iris is a framework for defining expressive program logics, which can be used to state and prove correctness and security properties for programs written in a variety of programming languages. Moreover, mathematical proofs about programs can be mechanically checked by a computer, which is important because proofs about programs involve many details. Thus, it is helpful that the computer can check that they have all been considered correctly.

The awardee papers are:

• 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). 

Since Iris was first developed (published in papers 2015-2018), it has been used in more than 65 research papers. Iris has not only been used in academia, but also in industry, e.g., by engineers at Meta to verify the core components of an interprocess communication system for a new operating system.

For more information about Iris, see iris-project.org