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


To apply, please send your application to Robbert Krebbers directly. The application must include:

Review of applications will begin immediately.

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

Informal inquiries to Robbert Krebbers are welcome.