PhD studentship in homotopy type theory and univalent foundations

Note: this position has been filled.

The TU Delft Department of Software Technology has a open position for a PhD student in Programming Languages, working with Benedikt Ahrens.

The starting date for the position could be as soon as September 1, 2021.

Code: TUD01190

About Homotopy Type Theory and Univalent Foundations

Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory.

Topics in HoTT/UF

Despite a flurry of discoveries in HoTT/UF in recent years, many open questions remain. Possible PhD projects include

  • Syntax and semantics of type theories,
  • Formalization and mechanization of results from mathematics and computer science in univalent foundations / two-level type theory,
  • Design and implementation of domain-specific type theories,
  • Univalence principle and its applications.

The PhD student should have knowledge in some of the following areas:

  • Type theory
  • Category theory
  • Computer proof assistants
  • Functional programming

and be interested in learning in the other areas.

About the Position

A fully funded PhD position is open for an excellent candidate working in an area related to HoTT/UF. The PhD student will be supervised by Benedikt Ahrens.

Conditions of Employment

Fixed-term contract: 4 years.

TU Delft offers a customisable compensation package, a discount for health insurance and sport memberships, and a monthly work costs contribution. Flexible work schedules can be arranged. An International Children’s Centre offers childcare and an international primary school. Dual Career Services offers support to accompanying partners. Salary and benefits are in accordance with the Collective Labour Agreement for Dutch Universities: Gross salary PhD student ranging from € 2.395,– (1st year) to € 3.061,– (4th year) per month, plus holiday allowance (8%) and end-of-year bonus (8.3%).

As a PhD candidate you will be enrolled in the TU Delft Graduate School. TU Delft Graduate School provides an inspiring research environment; an excellent team of supervisors, academic staff and a mentor; and a Doctoral Education Programme aimed at developing your transferable, discipline-related and research skills. Please visit for more information.

The Organization

The Programming Languages Research Group is an internationally leading research group in programming languages, and active in areas such as language engineering, language design, domain-specific languages, software verification, and program logics. The section employs over 15 people, including academic staff, around 10 PhD students, and two postdoctoral researchers. The group is responsible for programming and programming languages education at the bachelor and master’s levels in the TU Delft Computer Science curriculum.

The Software Technology (ST) Department is one of the leading Dutch departments in research and academic education in computer science, employing over 150 people. The ST Department is responsible for a large part of the curriculum of the bachelor’s and master’s programmes in Computer Science as well as the master’s programme Embedded Systems. The inspiration for its research topics is largely derived from technical ICT problems in industry and society related to large-scale distributed processing, embedded systems, programming productivity, and web-based information analysis.

The Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) is known worldwide for its high academic quality and the societal relevance of its research programmes. Offering an international working environment, the faculty has more than 1100 employees (including about 500 PhD students) and more than 3000 bachelor’s and master’s students. Together they work on a broad range of technical innovations in the fields of electrical sustainable energy, microelectronics, intelligent systems, software technology, and applied mathematics. Additional Information

For more information about this position contact Benedikt Ahrens (

Application procedure

To apply, please send your application letter by e-mail as soon as possible to Benedikt Ahrens ( including in the subject the position code “TUD01190”. It is highly recommended to get in touch informally prior to submitting an application.

All applications should include a PDF attachment with:

  • an application letter, including a statement of research interests that demonstrates an understanding of one or more areas of relevance to the PhD topic,
  • a detailed CV (including list of publications if available),
  • a list of courses taken and grades obtained,
  • a copy or link to your Master’s thesis,
  • contact details of 2-3 references.