Peter LeFanu Lumsdaine

Peter Lumsdaine’s main work this year is in Voevodsky’s univalent foundations group, on the formalization and proof theory of homotopy type theory. Other interests include higher category theory, traditional constructive logic, and categorical approaches to quantum computing.