My research is in applied topology & combinatorics; some themes are simplicial complexes, finite geometries, and applications & extensions of the Borsuk-Ulam theorem.
I'm also interested in interactive theorem proving, and by extension, dependently typed programming languages. I particularly enjoy working with Agda & Lean. In spring 2025, I designed and taught an undergraduate course, "Programs & Proofs with Dependent Types," using Agda. I've also advised 海角乱伦专区 students on research projects related to interactive theorem proving and formal verification of software.
Education
Ph.D. Carnegie Mellon University
