PhD Position: Multimodal Theory: KU Leuven is offering a PhD researcher position in the field of computer science with a focus on the implementation of modal type theory in Agda. The position offers an exciting opportunity for candidates with a strong background in mathematical logic and theoretical computer science, with a specific interest in functional programming, machine-checked formal proving, and programming language design. The selected researcher will contribute to advancing theoretical work and the development of modal features in Agda, benefiting both theoretical and applied researchers.
PhD Researcher Position: Implementation of Multimodal Type Theory for Agda
Summary Table
| Position | PhD Researcher in Multimodal Type Theory for Agda |
|---|---|
| Location | KU Leuven, Belgium |
| Department | Distributed and Secure Software (DistriNet) |
| Application Deadline | November 15 |
Study Area
The position is focused on the intersection of mathematical logic and theoretical computer science, with specific applications in functional programming, type theory, and category theory. Research will center around modal type theory and its implementation in the Agda proof assistant.
Scholarship Description
The PhD position offers the chance to work within a specialized team at KU Leuven, a globally renowned university in computer science research. The scholar will be involved in advancing the implementation of Multimodal Type Theory (MTT) in Agda, contributing to theoretical unification and practical application of modal systems. The position includes opportunities for research visits, conference attendance, and interaction with the Agda development community.
You will have access to a multicultural environment in Leuven, Belgium, and join a division that works closely with cybersecurity and software verification teams.
Eligibility
- Master’s degree in a field relevant to mathematical logic or theoretical computer science.
- Familiarity with functional programming (especially Haskell), type theory, and category theory is highly desirable.
- Goal-oriented, analytical, and creative thinker.
- Fluent in English (written and oral communication).
- Willingness to collaborate with international researchers and the Agda community.
- Ability to plan, execute, and report research independently.
Required Documents
- CV.
- Motivation letter.
- Bachelor’s and Master’s diploma transcripts.
How to Apply
To apply, send your CV, motivation letter, and diploma transcripts to Andreas Nuyts and Dominique Devriese via email (firstname.lastname@kuleuven.be) by November 15.
For questions or more information, feel free to contact the supervisors via email.
Last Date
November 15.
