My research focuses on the deep connections between type theory, homotopy theory, and category theory, exploring how these frameworks provide new foundations for mathematics and connect to computational logic.
Investigating the connections between homotopy theory and type theory, exploring univalence, higher inductive types, and new foundations for mathematics.
Studying categorical structures, ∞-categories, and their role in understanding mathematical foundations and the structure of mathematical objects.
Exploring dependent type systems, Martin-Löf type theory, and the computational interpretation of logical and mathematical constructions.
Developing synthetic approaches to homotopy theory within type-theoretic frameworks, enabling direct reasoning about homotopical structures.
Applying type-theoretic methods to formal proof systems and computer-verified mathematics, bridging theory and computational practice.
Examining fundamental questions about mathematical foundations, exploring alternatives to set theory and new axiom systems.
My doctoral work focused on convergent sequence properties of topological groups across various compactness properties, studying the interaction between algebraic and topological structures.
These areas represent an ongoing exploration of how modern mathematical frameworks can provide deeper insights into the nature of mathematical truth and computation. The intersection of homotopy type theory and computer science offers exciting possibilities for both pure mathematics and practical applications in formal verification, proof assistants, and the foundations of programming languages.