The Alonzo Church Award for Outstanding Contributions to Logic and Computation was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS) (until 2022). The award is for an outstanding contribution represented by a paper or small group of papers within the past 25 years.
The 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation
The European Association for Computer Science Logic (EACSL), the European Association for Theoretical Computer Science (EATCS), and the ACM Special Interest Group for Logic and Computation (SIGLOG) are pleased to announce that the 2023 Alonzo Church Award for Outstanding Contributions to Logic and Computation is given jointly to
- Lars Birkedal, Aleš Bizjak, Derek Dreyer, Jacques-Henri Jourdan, Ralf Jung, Robbert Krebbers, Filip Sieczkowski, Kasper Svendsen, David Swasey and Aaron Turon
for the design and implementation of Iris, a higher-order concurrent separation logic framework.
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, Ales 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, Ales Bizjak, Lars Birkedal, Derek Dreyer: “Iris from the ground up: A modular foundation for higher-order concurrent separation logic”. J. Funct. Program. 28 (2018).
Iris is a unifying framework that is at the same time rigorously founded and elegantly constructed, but also powerful and broadly applicable. Uniquely, Iris can explain a great variety of primitives in terms of a generic logic with a handful of well-understood mechanisms and comes with a mature implementation in the form of a Coq library. Iris has been very influential and has been applied for reasoning about a diverse range of systems, including fine-grained concurrency, weak memory, various type systems (recursive types, ownership types, gradual types, session types etc.), assembly languages, object capabilities, probabilistic languages, distributed systems and last but not least, models of practical languages like Rust, Scala and OCaml. Its features like higher-order ghost state, atomic invariants, guarded recursion have been used to implement program logics for partial and total correctness, but also unary and relational logical relations, and have in many cases made it possible to significantly advance the state of the art for applying those techniques. In addition to the development of Iris itself, Iris is at the core of a vibrant community. The Coq implementation is developed as open source software with regular releases. Course material has been developed, live tutorials have been taught and two dedicated Iris Workshops have been organised.