"PhD Position in the Semantics of Homotopy Type Theory"

The Institute for Logic, Language and Computation (ILLC) at the University of Amsterdam is inviting applications for a fully funded PhD position in the NWO project "Simplicial type theory" led by Dr. Benno van den Berg.

Join our research team! We are looking for a PhD candidate to conduct cutting-edge research at the intersection of mathematics and computer science.

What are you going to do? A key step in the development of homotopy type theory was the construction by Voevodsky of a model of this theory in simplicial sets. The purpose of this project is to develop a constructive account of this model based on the theory of effective Kan fibrations. Using this, we will develop a new simplicial type theory.

Your profile: MSc degree (or equivalent) in a relevant discipline, such as Mathematics, Logic, or Theoretical Computer Science; Familiarity with category theory; Excellent written and spoken English; Ability to work independently and collaboratively.

Our offer: A temporary contract for 38 hours per week for the duration of 4 years (initial 18 months, extendable after evaluation). Starting date around January 2026. Gross monthly salary between €3,059 and €3,881 (scale P), plus holiday allowance and year-end allowance. The UFO profile PhD Candidate applies.

Location: Science Park 904, 1098XH, Amsterdam.

Where you will work: The Faculty of Science at the University of Amsterdam, with a focus on interdisciplinary study at the ILLC.