I am a mathematician with a deep fascination for the foundations of mathematics and their connections to logic and computation. My work focuses on homotopy type theory, a revolutionary approach to mathematical foundations that unifies ideas from algebraic topology, category theory, and computer science.
I earned my PhD in Mathematics from Wesleyan University in Middletown, Connecticut, where I was trained as a topologist. My doctoral research focused on compactness and convergent sequence properties of topological groups, exploring the deep connections between algebraic and topological structures.
This topological training provided the perfect foundation for my current work in homotopy type theory. Topology—the study of continuous transformations and the fundamental nature of space—naturally connects to homotopy theory, which studies spaces up to continuous deformation. My background in topological groups, where algebraic and topological structures interact, prepared me to understand how different mathematical frameworks can be unified.
My current research explores the deep connections between homotopy theory and type theory, particularly the univalence axiom and its implications for mathematical foundations, higher inductive types and their role in synthetic homotopy theory, and the formalization of mathematical theorems in type-theoretic frameworks using proof assistants.
I am also interested in ∞-categories and their relationship to type theory and homotopy theory, as well as broader questions about the foundations of mathematics and alternatives to traditional set-theoretic foundations.
Beyond pure mathematics, I have over 25 years of experience in software engineering, having built complex distributed systems and architected large-scale software projects. This practical experience complements my theoretical work, giving me insight into how mathematical ideas can be implemented computationally.
This combination is particularly valuable in homotopy type theory, which is inherently computational. The proofs we construct in type theory are not just abstract arguments—they're programs that can be executed and verified by computers. Understanding both the mathematical theory and the computational practice allows me to bridge these two worlds effectively.
Homotopy type theory isn't just an abstract mathematical curiosity—it represents a fundamental rethinking of how we approach mathematical foundations. It offers new insights into the nature of mathematical objects, provides a computational interpretation of classical results, and opens pathways to verified mathematics and software.
As we build increasingly complex mathematical theories and software systems, having rigorous foundations that are both mathematically sound and computationally implementable becomes ever more important. This is the promise of homotopy type theory, and the challenge that drives my research.