PhD Position in Categorical Foundations of Type Theory

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.
Your responsibilities will include:

• conducting this research, both individually and as part of a team;
• participating in scientific life at Utrecht University and in the Netherlands, for example by 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.

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.

• 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;
• a 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 a range of its own schemes for employees. This includes arrangements for professional development, various types of leave, and options for sports and cultural activities. You can also tailor your employment conditions through our Terms of Employment Options Model. In this way, we encourage you to keep investing in your personal and professional development. For more information, please visit Working at Utrecht University.

A better future for everyone. This ambition motivates our scientists in executing their leading research and inspiring teaching. At Utrecht University, the various disciplines collaborate intensively towards major strategic themes. Our focus is on Dynamics of Youth, Institutions for Open Societies, Life Sciences and Pathways to Sustainability. Sharing science, shaping tomorrow.

Working at the Faculty of Science means bringing together inspiring people across disciplines and with a variety of perspectives and backgrounds. The Faculty has six departments: Biology, Pharmaceutical Sciences, Information & Computing Sciences, Physics, Chemistry and Mathematics. Together, we work on excellent research and inspiring education. We do so, driven by curiosity and supported by outstanding infrastructure. Visit us on LinkedIn and discover how you can become part of our community.

You will be employed jointly by the Department of Mathematics and the Department of Information and Computing Sciences. Within the Departement of Mathematics, you will be part of the Logic group. In addition to type theory and category theory, research in this group focuses on the formalization of type theory in Lean and the use of proof assistants in mathematics education. The department also includes a strong Homotopy theory group with research in higher category theory. In the Department of Information and Computing Sciences, you will be part of the Software Technology group. Research in this group focuses on using and improving functional programming languages such as Haskell and Agda, in particular for parallel computing, software testing, and language-based security.

For more information, please contact Paige Randall North at p.r.north@uu.nl

Do you have a question about the application procedure? Please send an email to science.recruitment@uu.nl.