My research sits at the boundary of higher category theory, homotopy theory, and the theory of programming languages and type systems. A central theme is understanding how ideas from algebraic topology and higher algebra can be made precise and computational through type-theoretic and proof-theoretic methods. I'm also interested in how these ideas might be applied in formal verification and programming language design.

In 2022, Tom de Jong and I started ASSUME, a joint seminar series between the universities of Birmingham and Nottingham intended to serve as a forum for research in Univalent mathematics.