PhD Position in Computing Sciences

Utrecht University

Netherlands

Faculty: Faculty of Science
Department: Department of Information and Computing Sciences
Hours per week: 36 to 40
Application deadline: 6 April 2026

Project Overview

Over the past decades, dependent type theory has been very successful as a programming language for writing and checking mathematical proofs. More recently, variations have been proposed for specific mathematical domains: homotopy type theory, cubical type theory, simplicial type theory, etc. These rely on a fundamental connection between mathematics and computer science. In this project, we seek to better understand this connection and to leverage it to create a theory of type theories.

Your Job

In this project, we see the aforementioned connection between mathematics and computer science as one between category theory and functional programming languages. Whereas the connection between mathematics and Martin-Löf type theory can be formalized as an equivalence between structured categories (e.g., comprehension categories, categories with families, or the like) and Martin-Löf type theories. We envision that the analogous correspondence for domain-specific variations on Martin-Löf type theory must incorporate more structured categories (e.g., enriched versions of comprehension categories or the like).

Your research will explore this area, allowing you to shape your own focus, potentially involving:

Exploring categorical semantics for these type theories using the tools of enriched category theory
Developing a common framework for these semantics
Formalizing aspects of this research
Formalizing mathematics within one of these type theories
Implementing aspects of this research

You will be supervised mainly by Paige Randall North, with co-supervisors selected as appropriate. You will be employed jointly by the Department of Mathematics and the Department of Information and Computing Sciences.

Responsibilities

Conducting this research, both individually and as part of a team
Participating in scientific life at Utrecht University and in the Netherlands, e.g., attending and organizing seminars
Participating in scientific life more globally, including publishing papers and attending workshops and conferences
Contributing to teaching in mathematics and computer science, providing the opportunity to gain teaching experience

Required Qualifications

We are looking for a new colleague who:

Holds a Master’s degree in mathematics or computer science
Has a solid foundation in category theory
Is familiar with dependent type theory
Is enthusiastic about learning advanced category theory and applying it to understanding the foundations of type theory
Has strong English skills, both in speaking and in writing

Terms of Employment

A position for 18 months, with an extension to a total of four years upon successful assessment in the first 18 months
A gross monthly salary starting at €3,059 in the first year and increasing annually up to €3,881 in the fourth year, based on full-time employment (salary scale P under the Collective Labour Agreement for Dutch Universities (CAO NU))
8% holiday pay and 8.3% year-end bonus
Pension scheme, partially paid parental leave, and flexible terms of employment based on the CAO NU

In addition to the terms of employment laid down in the CAO NU, Utrecht University also offers professional development schemes, various types of leave, and options for sports and cultural activities. Employment conditions can be tailored through the Terms of Employment Options Model.

About Utrecht University

A better future for everyone motivates our scientists in executing leading research and inspiring teaching. Various disciplines collaborate intensively towards major strategic themes, including Dynamics of Youth, Institutions for Open Societies, Life Sciences, and Pathways to Sustainability.

The Faculty of Science brings together inspiring people across disciplines. It includes six departments: Biology, Pharmaceutical Sciences, Information & Computing Sciences, Physics, Chemistry, and Mathematics. Research areas include type theory, category theory, formalization in Lean, homotopy theory, and functional programming languages like Haskell and Agda.