by Ankita Atrey
10 March 2025 · 4 min read

In October 2024, Daniel Gratzer joined Aarhus University as a Tenure-Track Assistant Professor in the Logic and Semantics group. Daniel kicked off his academic journey with a bachelor’s degree from Carnegie Mellon University, diving into the world of programming languages. He started with applied areas like compilers and functional programming, but over time, his curiosity led him deeper into the theoretical side of things. This spark drove him to pursue a PhD at Aarhus University, where he thrived in a vibrant community of thinkers, exploring programming languages and type theory under the expert guidance of Lars Birkedal. After wrapping up his PhD in 2023, Daniel continued his research adventure with a postdoctoral position in Aarhus University and visiting researcher at Oxford University.

His primary research focus is on type theory and category theory, with particular interest in higher category theory and model dependent type theory, which define the core of his work.

Can you tell us about your current research?
I study programming languages and type theories through the lens of category theory, with a specific focus on dependent type theory, particularly modal and homotopy type theory. While I am broadly interested in these areas, my research aims to apply concepts from the theory of programming languages to improve both mathematics and software engineering. My goal is to make mathematics more accessible for mathematicians and enhance software development.

What challenges do you face in your research?
I see two major challenges:

• Mathematical challenge: Mathematics is inherently difficult, and proving theorems can often be a slow and frustrating process.
• Sociological challenge: Bridging the gap between different disciplines, such as computer science and mathematics, is challenging. For example, in my work on synthetic infinity category theory, we aim to collaborate with both computer scientists and mathematicians. However, these two groups often speak different languages, making effective communication and collaboration a challenge.

How do you see the impact of your research on various fields?
I hope my reseaech will have significant impact on the world of software development. As software becomes more complex, there is a growing need for more reliable tools and robust languages to express ideas. Concepts derived from category theory, such as univalence, are already making an impact in structuring and verifying programs, although this is still in the early stages

Do you have any hobbies outside of work?
Outside of work, I enjoy reading and rock climbing, seemingly the two hobbies most embraced by computer scientists!

What motivated you to choose Aarhus university?
I chose to join Aarhus University because I had been living here for a while and really enjoyed the city. Additionally, the department has a strong group of people working on a diverse range of exciting projects in programming languages. This environment fosters exposure to different areas of research and allows for valuable feedback, rather than being confined to one narrow niche.