I’m an assistant professor 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.
Recent news
September 2021: Synthetic Cohomology Theory in Cubical Agda accepted to CSL 2022.
September 2021: New preprint Implementing a category-theoretic framework for typed abstract syntax (PDF coming soon).
September 2021: Lecture notes on cubical type theory for the 2019 HoTT Summer School accepted for publication in MSCS (the notes can be found here).
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 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