Benedikt Ahrens, who co-supervised my PhD, has funding for a PhD position at TU Delft 🙂️ I'm copying his ad below. I highly recommend both Delft and Benedikt!
#TypeTheory #Agda #CategoryTheory #PhD
----------
I am looking for a PhD candidate for a 4-year position in the Department of Software Technology at TU Delft, funded by the Air Force Office of Scientific Research (AFOSR) and starting as soon as possible.
The project, "SemSyn: From Semantics to Syntax", studies how to start from a specification of a class of models and derive a formal language describing them. It involves:
- dependent type theory and its categorical semantics (categories with families, comprehension categories);
- generalized algebraic theories;
- Makkai's signatures, given by inverse categories;
- two-level type theory;
- formalization in the Agda proof assistant, developed alongside the mathematics.
You should have a Master's degree in mathematics, computer science, or a related field, and experience in (or a strong motivation to learn) both category theory and theoretical computer science. Experience with a proof assistant is a plus, but not required.
Applications are evaluated on a rolling basis, so please apply early rather than waiting for the deadline of 29 November 2026. I very much encourage you to get in touch with me by email ([email protected]) before, and in addition to, submitting your official application.
Vacancy and application: https://careers.tudelft.nl/job/Delft-PhD-Position-Systematic-Derivation-of-Formal-Languages-and-Their-Correctness-2628-CD/1375074157/