Dear All, 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: https://careers.tudelft.nl/job/Delft-PhD-Position-Systematic-Derivation-of-F... Please forward this message to anyone who might be interested. All the best, Benedikt