PhD Position in Systematic Derivation of Formal Languages
Explore the systematic mathematical derivation of formal languages and type theories using Agda.
Best for:Best for candidates with a Master's degree in mathematics or computer science and a strong background in category theory, type theory, or formal verification.
Overview
This 4-year PhD position at Delft University of Technology investigates how to systematically derive formal languages, such as type theories and program logics, directly from their mathematical semantics rather than designing them by hand. Working within the Department of Software Technology under the supervision of Dr. Benedikt Ahrens, the candidate will employ tools from category theory and type theory while formalizing and checking their results using the Agda proof assistant. The role involves independent and collaborative research, publishing findings, participating in academic seminars, and contributing to computer science teaching. The successful applicant will receive structured doctoral training within the TU Delft Graduate School in an inspiring and collaborative environment.
What you'll do
- Conduct independent and collaborative research on the systematic derivation of formal languages from semantics
- Develop and verify theoretical models using category theory and type theory within the Agda proof assistant
- Participate actively in the scientific life of the department, including attending and organizing seminars
- Disseminate research results by publishing papers in peer-reviewed venues and attending international conferences and workshops
- Contribute to teaching activities in computer science and assist with student supervision
Requirements
Degree required: Master's degree in mathematics, computer science, or a related field
Degree offered: PhD
Language: English; excellent written and spoken proficiency
Instruction: English
- Strong background or demonstrated motivation in category theory and theoretical computer science
- Familiarity with type theory, logic, or programming language semantics
- Passion for precise mathematical reasoning and proof development
- Ability to work independently and collaborate across the mathematics and computer science boundary
- Excellent written and spoken English communication skills
Funding & terms
How to apply
Deadline: 2026-11-29
Interested candidates should submit their application online through the official portal by the stated deadline. The application package must include a CV, a motivational letter, and relevant Master's degree transcripts.
- CV
- Motivational letter
- Master's degree transcripts
Contact
Benedikt Ahrens
Create a free profile to unlock your personal match score, the full requirements, funding details and how to apply — in English or Persian.