Nicolai Kraus

Nicolai Kraus is a Professor of Theoretical Computer Science and Royal Society University Research Fellow at the University of Nottingham, working in the Functional Programming Lab. He was previously a member of the Birmingham Theory Group and at Eötvös Loránd University.

He earned his PhD in 2015 from the University of Nottingham under the supervision of Thorsten Altenkirch, with his thesis titled "Truncation Levels in Homotopy Type Theory," for which he won the Ackermann award. His examiners were Julie Greemsmith (internal) and Steve Awodey (external).

Kraus works primarily in dependent type theory (with Agda as his favorite proof assistant), with a main focus on homotopy type theory and higher categories. His research extends to constructive and non-constructive mathematics more broadly, exploring the connections between different mathematical structures within type theory frameworks. He has made significant contributions to the understanding of higher inductive types, set quotients, and the implementation of type theory in proof assistants.

His recent publications demonstrate a consistent focus on homotopy type theory and its applications. His work explores the connections between type theory and classical mathematics, particularly in areas like ordinal arithmetic, higher categorical structures, and formal verification. He has developed novel approaches to coherence theorems, set-theoretic constructions in type theory, and the implementation of higher-dimensional structures.

He was awarded the Ackermann award for his PhD thesis on "Truncation Levels in Homotopy Type Theory."

Kraus currently supervises several PhD students and postdocs, including Aref Mohammadzadeh, Tom de Jong, Stiéphen Pradal, and Joshua Chen. He also serves as a second supervisor for Johannes Schipp von Branitz and Stefania Damato. Starting in 2025, he will lead an ERC (European Research Council) project in dependent type theory.

He is a member of the Functional Programming Lab at the University of Nottingham and has organized several academic events including the "Types, Thorsten and Theories" workshop, Midlands Graduate School events, and Agda Implementors' Meetings.