He obtained his PhD in computer science from Carnegie Mellon University in 2011 under the supervision of Robert Harper. His work in homotopy type theory has focused on the development and formalization of synthetic homotopy theory, and on new type theories inspired by higher categorical/homotopy-theoretic semantics, such as cubical, adjoint, and directed type theories.