I’m currently a postdoc in the School of Computer Science at Carnegie Mellon University. My main research interests are Homotopy Type Theory and Univalent Foundations, in particular computational justifications for univalence and higher inductive types using cubical type theory.

Before this I was a postdoc in the Marelle team at Inria Sophia-Antipolis. I also spent a year as a member of the School of Mathematics at the Institute for Advanced Study in Princeton working on formalization of mathematics in Univalent Foundations with Vladimir Voevodsky.

I defended my PhD thesis at the Department of Computer Science and Engineering at Chalmers University of Technology and University of Gothenburg under the supervision of Thierry Coquand in December 2014.

## Software

I’m actively developing and contributing to:

- cubicaltt - A Haskell implementation of a type theory based on a model in cubical sets. This system provides a computational interpretation to notions from Univalent Foundations and Homotopy Type Theory, most notably the univalence axiom.
- UniMath - A Coq library for formalizing mathematics using the univalent point of view.

I have previously developed:

- 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.