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.