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.

## Software

I’m actively developing and contributing to:

Cubical Agda - A version of Agda with cubical primitives making it into a full-blown proof assistant with support computational univalence and user defined higher inductive types.

UniMath - A Coq library for formalizing mathematics using the univalent point of view.

I have previously developed:

cubicaltt - A Haskell implementation of a type theory based on a constructive model in cubical sets. This system provides a computational interpretation to notions from Univalent Foundations and Homotopy Type Theory, most notably the univalence axiom. This has now been succeeded by Cubical Agda.

yacctt -

*yet another cartesian cubical type theory*. This is a version of cubicaltt based on Cartesian Cubical Type Theory. This has been succeeded by redtt.cubical - A predecessor of cubicaltt.

The Coq Effective Algebra Library (CoqEAL) - A library for conveniently combining proving and efficient computations in the Coq proof assistant.