Anders Mörtberg

Anders Mörtberg is an Associate Professor in Computational Mathematics at the Department of Mathematics, Faculty of Science, Stockholm University. He has been a faculty member since 2019 and was promoted to associate professor with tenure in April 2023. His research lies at the intersection of type theory, logic, and formal verification, with a focus on Homotopy Type Theory (HoTT) and Univalent Foundations.

His primary research interests include:

• Computational justifications for univalence and higher inductive types via cubical type theory
• Computer formalization of mathematics and computer science
• Constructive mathematics and logic
• Category-theoretic foundations
• Functional programming and proof assistants

His recent publications demonstrate a strong trend toward synthetic homotopy theory, cohomology, and algebraic structures formalized in Cubical Agda. He has made significant contributions to both theoretical developments and practical implementations, particularly in advancing Cubical Agda as a full-featured proof assistant. His work enables rigorous, machine-checked proofs in algebraic topology and constructive algebra.

Scientific awards include:

• Distinguished Paper Award at LICS 2023
• Distinguished Paper Award at CPP 2023
• Distinguished Paper Award at ICFP 2019

He advises several PhD students, including Axel Ljungström (main supervisor), Max Zeuner, Gabriel Saadia, Errol Yuksel, and Elisabeth Stenholm (external main supervisor). He has received competitive research grants from the Swedish Research Council (Vetenskapsrådet) and the Knut and Alice Wallenberg Foundation, supporting postdoctoral recruitment and foundational work on proof assistants. He regularly teaches courses such as Programming Paradigms and Programming for Mathematicians at Stockholm University.

He is a core developer of Cubical Agda, an extension of Agda with native support for univalence and higher inductive types, and has contributed to UniMath, cubicaltt, and yacctt. His software tools are widely used in the formal methods and type theory communities.