I’m an associate professor (docent) in the Computational Mathematics division at the Department of Mathematics at Stockholm University. My main research interests are currently in Homotopy Type Theory and Univalent Foundations, in particular computational justifications for univalence and higher inductive types using cubical type theory. I’m also interested in constructive mathematics, logic and type theory, category theoretical foundations, functional programming, and computer formalization of mathematics and computer science.
[ Google scholar | Github | Mathstodon ]
Some sporadically updated news
Feb 2024: new preprint Automating Boundary Filling in Cubical Agda with Maximilian Doré and Evan Cavallo.
Feb 2024: new preprint The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations with Daniel Gratzer, Håkon Gylterud, and Elisabeth Stenholm.
Jan 2024: new preprint Computational Synthetic Cohomology Theory in Homotopy Type Theory with Axel Ljungström.
July 2023: A Univalent Formalization of Constructive Affine Schemes published in the post-proceedings of TYPES 2022.
June 2023: Formalizing π4(S3)≅Z/2Z and Computing a Brunerie Number in Cubical Agda awarded Distinguished Paper Award at LICS 2023.
June 2023: obtained docent title in Computational Mathematics.
April 2023: promoted to associate professor (with tenure) in Computational Mathematics.
January 2023: Computing Cohomology Rings in Cubical Agda awarded Distinguished Paper Award at CPP 2023.
February 2022: Synthetic Integral Cohomology Theory in Cubical Agda published in post-proceedings of CSL 2022.
January 2022: Implementing a Category-theoretic Framework for Typed Abstract Syntax published in post-proceedings of CPP 2022.
September 2021: Lecture notes on Cubical methods in Homotopy Type Theory and Univalent Foundations written for the 2019 HoTT Summer School accepted for publication in MSCS.
April 2021: Gave a course about Cubical Type Theory and Cubical Agda at the EPIT spring school on HoTT. Material can be found here.
March 2021: awarded KAW postdoc recruitment grant.
December 2020: extended journal version of Cubical Agda paper Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types.
September 2020: new paper in POPL’21 Internalizing Representation Independence with Univalence.
November 2019: awarded with a starting grant from the Swedish Research Council (Vetenskapsrådet) for the project Cubical Methods for Computer Formalization of Mathematics
September 2019: started as assistant professor in the Department of Mathematics at Stockholm University