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
June 2021: Updated lecture notes on cubical type theory for the 2019 HoTT Summer School are available here. Comments and suggestions for improvements are very welcome!
April 2021: Gave a course about Cubical Type Theory and Cubical Agda at the EPIT spring school on HToT. Material can be found here.
March 2021: awarded KAW grant.
January 2021: new preprint Synthetic Cohomology Theory in Cubical Agda.
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