Robbert Krebbers

ERC Consolidator Project COCONUT

I have been awarded an ERC Consolidator Grant for the project Developing Correct Concurrent Software Using Types (COCONUT). This 5-year project starts 1 April 2025 and will include funding for several PhD candidates and postdocs, advised by Robbert Krebbers at the Department of Software Science of Institute for Computing and Information Sciences at Radboud University Nijmegen, The Netherlands.

Project members

Open positions

I am looking for PhD candidates with a background in programming language theory and/or verification. A master's degree in computer science, mathematics, or a related field is required. There is no need to have prior experience with Rocq or Iris (although that would be appreciated).

How to apply? I will be considering applications on a rolling basis. Please contact me (robbert AT cs DOT ru DOT nl) to submit an application, or if you want to learn more about the project. In your application email please include: (1) a description of why and in which parts of the project you are interested, (2) a description of your prior experience, (3) your CV, (4) contacts for recommendation letters, and (5) if possible, a copy of your master's thesis (do not hesitate to apply if your master's thesis is not finished yet).

Salary and conditions. PhD candidates will be employed for 4 years (with a go/no-go evaluation after 1.5 years) at Radboud University Nijmegen. We offer an attractive salary (the gross salary of a PhD candidate starts at 2.901 EUR per month, and increases to 3.707 EUR per month in the last year, based on a 38-hour working week, see salary scale P), excellent employment conditions (including 8% holiday allowance, 8% end-of-year bonus, extra days off), and moderate teaching obligations (around 10%). See https://www.ru.nl/phd for more information. PhD candidates on the CONONUT project will have access to ample travel funding (for international conferences, summer schools, research visits to collaborators, etc).

Postdocs. Although the postdoc position is scheduled to start in 2027, I am always on the look out for exceptional postdoc candidates with specialized experience in substructural type systems (especially Rust and session types), concurrent separation logic (especially Iris), interactive theorem proving (Rocq), compiler verification, and relaxed memory consistency. If you are interested, do not hesitate to contact me.

Summary

COCONUT Modern society runs on concurrent software: different processes (threads) jointly process massive data sets and serve many clients and users simultaneously. Good methods to ensure the correctness of concurrent software are lacking due to the enormous space of concurrent executions. But it is vital to have some correctness guarantees, e.g., "every thread will eventually perform an action" (liveness) or "private data cannot leak to an attacker" (non-interference). Recent years saw an active development and industry adoption of new programming languages that automatically enforce correctness guarantees through a type system that disables programmers from writing "bad programs". Yet, existing concurrent programming languages (such as Rust) cannot enforce "deep" concurrency properties such as liveness and non-interference. Moreover, there is no guarantee that the good properties of high-level programs are preserved after compilation to executable machine code, because compilers perform increasingly complicated unverified optimizations.

The COCONUT project will design and verify new type systems, compilers and logical abstractions for fully-fledged concurrent programming languages that automatically enforce deep program properties. COCONUT will address this objective through rigorous machine-checked foundations (in Rocq), leveraging recent innovations in the development of powerful program logics for concurrency (such as Iris). The foundations are essential to prove the validity of our results, but they will also play a key role for experiments and to bring together recent results from the fields of programming language theory, concurrency theory, compilers, security and proof assistants.

The project consists of three work packages:

  1. Program logics for deep concurrency properties: We design, develop and verify program logics based on higher-order concurrent separation logic for deadlock freedom (program execution cannot end up in a state where all threads are waiting), resource leak freedom (all unused resources are deallocated), liveness (all threads can eventually perform an action) and non-interference (private data cannot leak to an attacker).
  2. Type systems for deep concurrency properties: Our program logics support arbitrary pre- and postconditions and are thus inherently undecidable. In this work package we use the logical approach to type soundness to layer types and typing rules on top of these logics that allow for automatic verification through type checking. We will do that by building on ideas from Rust, session types and type systems for non-interference.
  3. Compiler verification for deep concurrency properties: We will use relational versions of concurrent separation logic (extending ReLoC and Simuliris) to verify an optimizing compiler frontend from our high-level source languages to a lowered target language in which the concurrency primitives are replaced by efficient low-level implementations.

Funded by EU Funded by the European Union (grant agreement no. 101171349). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or European Research Council (ERC). Neither the European Union nor the granting authority can be held responsible for them.