My research lies broadly in category theory, logic, and constructive mathematics. Most of my recent work is within or related to the Homotopy Type Theory/Univalent Foundations programme: developing dependent type theory as a foundation for mathematics, drawing on ideas from homotopy theory and higher category theory.

I am also interested in quantum programming languages (I worked on the early stages of Quipper) and mathematical computing.

Publications & preprints