PhD position at TU Delft: deriving formal languages from their semantics
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 (B.P.Ahrens@tudelft.nl) before, and in addition to, submitting your official application.
Vacancy and application: PhD Position Systematic Derivation of Formal Languages and Their Correctness Job Details | TU Delft
Please forward this message to anyone who might be interested.