2023 Alonzo Church Award to Lars Birkedal

Congratulations to Professor Lars Birkedal and collaborators who will be presented with 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 Germany this summer.

Prof. Lars Birkedal
Prof. Lars Birkedal. Photo by Søren Kjeldgaard.

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:

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