Vacancies
Positions available
(Last updated: March 3, 2025.)
- PhD position: Cyclic proofs in coalgebraic modal logic (Details)
- PhD position: Coalgebraic modal type theory (Details)
- PhD position: Coalgebraic session protocols and Actris (Details)
- PhD position: Liveness from causality analysis (Details)
- PhD position: First-class coinduction in proof assistants (Details)
- PhD position: Liveness in types and program logics (Details)
The vacancies, in general
- The Netherlands is a very attractive place to do a PhD. PhD student positions in the Netherlands are fully-funded, four-year employed positions, typically structured as a one-year contract renewable for three years.
- PhD students enjoy full employee benefits (health insurance holiday, pension, etc). The online document “A beginner’s guide to Dutch academia” offers lots of further information and pointers.
- PhD students will be based in and employed by one of the universities involved in the project. They will have two co-supervisors, and will be given the opportunity of spending time in at least two different universities during their work in the project.
- PhD positions come with moderate teaching obligations (around 10%), to be arranged in accordance with the supervisor(s) and their own university.
- Each PhD position comes with generous funding reserved for attending summer schools, international conferences, project meetings, and research visits.
Application Instructions
- Deadline: TBD
- Instructions: TBD
- Further details: TBD
The Vacancies, in Detail
PhD Position: Cyclic proofs in coalgebraic modal logic
Main location: Groningen.
Detailed description to be added soon.
PhD Position: Coalgebraic modal type theory
Main location: Leiden.
Detailed description to be added soon.
PhD Position: Coalgebraic session protocols and Actris
Main location: Groningen.
Many verification techniques for interacting programs are based on process calculi. While most valuable, there is a wide gap between the (abstract) processes in those models of concurrency and the (concrete) interacting programs that can be analysed using proof assistants.
As a PhD student in this project, you will reduce the gap between these abstract and concrete perspectives by identifying rigorous connections between two salient approaches to verification that already support coinductive structures:
- Coalgebraic formulations of session types, which provide a general and expressive semantic framework for session type systems, subsuming previous (syntactic) approaches and inducing useful decidability results;
- Actris, a program logic for interacting programs, developed on top of the Rocq proof assistant (via the Iris logic), which enables the seamless analysis of message passing and other features (e.g., locks).
The two approaches are different (one is a type system, the other is a program logic) and so they analyse interacting programs at different levels of abstraction. Hence, the key challenge is identifying formal relationships between them, with two goals: (i) enabling cross-fertilisation of techniques and results and (ii) elucidating the status of Actris with respect to the large body of work on type systems for concurrency based on process calculi.
Key References
- Coalgebraic session protocols (TOPLAS’22)
- Actris (LMCS’22)
Locations
The Fundamental Computing group at University of Groningen (main location) and Radboud University Nijmegen.
Contact Persons
Jorge A. Pérez and Robbert Krebbers
PhD Position: Liveness from causality analysis
Main location: UTwente.
Detailed description to be added soon.
PhD Position: First-class coinduction in proof assistants
Main location: Delft.
Essential to writing and reasoning about software that operates continuously is a practically usable language for programs and proofs of coinductive types. Proof assistants currently rely on either syntactic guardedness conditions on programs, sized types, or guarded recursion. However, the syntactic guardedness condition is very restrictive and brittle, while both sized types and guarded recursion require significant additional annotations to the program.
As a PhD student in this project, you will work towards developing a new system for defining and reasoning about coinductive processes in proof assistants. The key challenge is to develop a system that is both modular (so productivity information is propagated through the type system) and user-friendly (so few or no manual annotations are needed).
This project combines and builds on existing approaches proposed in the literature:
- Sized types and guarded type theory, in particular their implementation in Agda.
- Coinductive reasoning in (higher) observational type theory and cubical type theory.
In order to ensure soundness and usability, this project will require a combination of theoretical analysis of a type theory with first-class reasoning about coinductive processes and the development of a prototype implementation of this type theory as an extension to Agda.
Key References
- Wellfounded recursion with copatterns: a unified approach to termination and productivity (ICFP’13)
- Productive coprogramming with guarded recursion (ICFP’13)
Location
The Programming Languages Group at TU Delft
Contact Persons
PhD Position: Liveness in types and program logics
Main location: Nijmegen.
As a PhD student in this project, you will work towards developing methods to ensure liveness of complex systems that use a combination of:
- Interaction with environment (input/output), e.g., file system, system calls, network, external devices, and
- Concurrency, both system-level (hardware threads) and cooperative (aka async, aka lightweight threads).
The key challenge is to obtain compositional reasoning methods, which allow the reduction of liveness proofs to properties of sub-systems.
The starting point is the framework of interaction trees for monadic semantics of programs that interact with their environment. In order to deal with concurrency, we will build on the choice tree extension that enhances interaction trees with cooperative concurrency. Building on this semantics, we will develop a logic based on Iris that allows us to specify program interactions. We will obtain refinement type system for automating large parts of liveness verification by enhancing the existing session types in Actris/Iris. The resulting logic and type system will be implemented in the Rocq proof assistant.
Key References
Locations
The Software Science Group at Radboud University Nijmegen (main location) and University of Groningen.