PhD position in Type Systems for Concurrency at University of Groningen [NL]

Applications are now open for one fully-funded PhD position on type systems for concurrency, co-supervised by Jorge Pérez and Dan Frumin (Groningen) and Robbert Krebbers (Nijmegen). The successful candidate will explore the semantic foundations of type systems for message-passing concurrency (e.g., session types), employing techniques like logical relations and coalgebras, and establishing rigorous connections with frameworks like Iris and program logics like Actris.

The ideal candidate has proven research experience in one or more of the following: semantics of programming languages, concurrency theory, type systems, logics such as linear logic and separation logic, and proof assistants. Prior knowledge of session types and Rocq/Iris is not a prerequisite, but it would be an advantage.