Robbert Krebbers


The Programming Languages group at Delft University of Technology is looking for:

The topic of research, which will be determined based on the common interests of the candidate and the supervisor, will be in the development of expressive program logics for:

This work will revolve around Iris: a higher-order concurrency separation logic framework that is implemented in the Coq proof assistant. Iris has been successfully used for a variety of applications including but not limited to logical-relations for relational reasoning, program logics for relaxed memory models, program logics for object capabilities, and a safety proof for a realistic subset of the Rust programming language.

The successful candidates will work under the supervision of Robbert Krebbers and Eelco Visser.

Requirements for the PhD position

Requirements for the post-doc position


I will be considering applications until the positions are filled. If you are interested in one of the positions, please contact me directly at (λ x y . mail @ x y . nl) robbert krebbers.

For the PhD position, please apply here by submitting a detailed CV, contact information for two references, a letter of motivation and a detailed transcript of university grades. Please also attach a (draft) version of your Master thesis.

For the postdoc position, please apply to me directly by sending a detailed CV (containing a list of publications), the contact information for two references, and a research statement.

The starting date of both positions will be decided with the candidate (earlier dates are preferred).