Positions available

(Last updated: 20 March 2025)

  1. PhD position: Cyclic proofs in coalgebraic modal logic (Details)
  2. PhD position: Coalgebraic modal type theory (Details)
  3. PhD position: Coalgebraic session protocols and Actris (Details)
  4. PhD position: Liveness from causality analysis (Details)
  5. PhD position: First-class coinduction in proof assistants (Details)
  6. 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 #1: Cyclic proofs in coalgebraic modal logic

Main location: Groningen.

In formal verification, system properties are often expressed in modal fixpoint logics such as LTL, CTL or modal μ-calculus. In recent years, cyclic proof systems for such logics have received much attention and led to new, constructive methods for proving logical properties such as completeness and interpolation, which are useful for automated reasoning. Cyclic proof systems have also been applied in verification methods such as model checking.

Coalgebraic modal logic is a powerful abstract framework in which modal logics can be developed for a wide range of system types in a unified setting using category theory. This means that results can be proved at the abstract coalgebraic level, and instantiated for concrete system types and logics. The model theory of coalgebraic modal (fixpoint) logics is well-developed, but the proof theory less so, and in particular, there are no cyclic proof systems (yet) for coalgebraic modal logic.

As a PhD student in this project, you will develop cyclic proof theory for coalgebraic modal fixpoint logics, with the aim to prove general results on completeness and interpolation, and make the cyclic proof methods available to a range of domain-specific languages. The starting point will be the recent literature on cyclic proof theory, and understanding how these methods can be lifted to the coalgebraic level.

Key References

  • Bahareh Afshari, Graham E. Leigh & Guillermo Menéndez Turata: Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus (TABLEAUX 2021)
  • Clemens Kupke, Dirk Pattinson: Coalgebraic semantics of modal logics: An overview (TCS, 2011)
  • Takeshi Tsukada and Hiroshi Unno: Software Model-Checking as Cyclic-Proof Search (POPL, 2022)

Locations

The Fundamental Computing group at University of Groningen (main location) and Leiden University.

Contact Persons

Helle Hvid Hansen and Henning Basold

PhD Position #2: Coalgebraic modal type theory

Main location: Leiden.

Coalgebraic modal logic is a powerful abstraction of logic for reasoning about systems that can be described as coalgebras. The current focus of coalgebraic modal logic is on rich formulas and semantics, while it is lacking a general theory of proof objects and certified proofs. This hampers the usability of coalgebraic modal logic for the verification of large systems using proof assistants.

As a PhD candidate in this project, you will devise a framework of general type theories for coalgebraic modal logic that are parametric in the behaviour to be reasoned about and feature inductive-coinductive types. Being parametric allows for domain-specific theories, while inductive-coinductive types will allow us to express global and path properties as cyclic formulas analogous to µ-calculi. As such, you will also be closely working with the PhD candidate in Project A1. A key challenge is expressing parametric behaviour, axioms and semantics, while retaining soundness when combining with other type-theoretic features like dependent types. This combination is essential, as dependent type theory is the foundation of many proof assistants.

Key References

  • Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, and Lars Birkedal: Modalities and Parametric Adjoints (ACM TOCL, 2022)
  • Michael Shulman: Semantics of Multimodal Adjoint Type Theory (MFPS, 2023)
  • Ryota Kojima, Corina Cîrstea, Koko Muroya, and Ichiro Hasuo: Coalgebraic CTL: Fixpoint Characterization and Polynomial-time Model Checking (CMCS, 2024)

Locations

The STyLo Team at the Leiden Institute of Advanced Computer Science of the Leiden University (main location) and TU Delft.

Contact Persons

Henning Basold and Jesper Cockx

PhD Position #3: 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

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 #4: Liveness from causality analysis

Main location: UTwente.

Pinpointing and explaining the root-cause of failures in interacting programs is key to ensure fault-tolerance. Although existing formalisms enable reasoning about safety (e.g., via reachability analyses), liveness is much harder to track: distinguishing between actual termination and a deadlocked configuration requires identifying some practical boundaries that ensure sound yet feasible analyses.

As a PhD student in this project, you will work on devising causal machineries able to detect, explain and facilitate recovery from liveness violations. Such frameworks will:

  • Answer questions such as “what caused the violation breach?”, “who is responsible for the breach?” or “did the breach of liveness cause any harm?”
  • Enable recovery strategies based on counterfactuals (“what if”) that can be used to guide an interacting program that breaches liveness back to a valid state.

The starting point is to identify realistic constraints (e.g., fairness assumptions, timeout mechanisms) that enable the analysis of liveness violations by means of appropriate extensions of coalgebraic session types. The latter describe the behaviour of communication channels in interacting programs. Then, a corresponding definition of causality will be obtained by establishing formal connections between (i) the behavioural maps underlying (extended) coalgebraic sessions and (ii) relevant causal models proposed in the literature. Eventually, we will devise algorithms for causality-based analysis of liveness violations, and recovery mechanisms based on counterfactuals.

Key References

Locations

The Formal Methods and Tools Group at the University of Twente.

Contact Persons

Georgiana Caltais

PhD Position #5: 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

Jesper Cockx

PhD Position #6: 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:

  1. Interaction with environment (input/output), e.g., file system, system calls, network, external devices, and
  2. 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.

Contact Persons

Robbert Krebbers