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

April 2020: We are hiring PhD students in Computational Mathematics! For details see https://www.su.se/english/about/working-at-su/phd?rmpage=job&rmjob=11944&rmlang=UK

March 2020: Lecture notes for the 2019 HoTT Summer School available here. Comments and suggestions for improvements are very welcome!

July 2020: Carlo Angiuli and I are organizing a session on Univalent Mathematics: Theory and Implementation at ICMS 2020.

~~May 2020~~: I will be teaching about Cubical Type Theory and Cubical Agda at the EPIT summer school on HoTT. This has moved to October 2020.

Spring 2020: teaching Programming Paradigms at Stockholm University

November 2019: awarded with a starting grant from the Swedish Research Council (Vetenskapsrådet) for the project

*Cubical Methods for Computer Formalization of Mathematics*(3.6M SEK over 4 years)September 2019: started as assistant professor in the Department of Mathematics at Stockholm University