Research

• Writing
• Talks
• Notes

Professionally, I’m a mathematician working at the junction of math, logic and computer science.

I study the programming languages and logics called homotopy type theories, as well as the mathematical structures known as higher or infinity categories. My research aims to develop type theoretic tools to reason about, and compute with, the categorical structure that underlies mathematical, software, and physical systems.