The award citation is as follows: Higher-Order Ghost State represents a major milestone for the widely used Iris program logic framework. Colloquially known as “Iris 2.0”, the paper contributes a key feature: the ability to store arbitrary higher-order separation logic predicates in ghost variables. The feature is justified using guarded recursion and a new algebraic structure called cameras - roughly, a generalization of PCMs with a form of step indexing.
Higher-Order Ghost State was later shown to be an essential building block from which other features like impredicative invariants and weakest preconditions could be derived. Its broad and lasting impact is evident in the (currently) 165 papers that use Iris in some way, including 45 POPL, 29 PLDI, 25 ICFP, and 20 OOPSLA papers.
Robbert Krebbers has received the 2026 Most Influential ICFP Paper Award
Robbert Krebbers has received the 2026 ACM SIGPLAN Most Influential ICFP Paper Award for his International Conference on Functional Programming (ICFP) 2016 paper Higher-Order Ghost State, co-authored with Ralf Jung, Derek Dreyer, and Lars Birkedal. The award is given to a paper, which was presented at the ICFP held 10 years prior to the award year, for its lasting impact on programming languages research.
Contact information
- Organizational unit
- Institute for Computing and Information Sciences
- About person
- Prof. R.J. Krebbers (Robbert)