NSF Postdoctoral Fellow
Department of Mathematics
Massachusetts Institute of Technology
I am working on automation techniques in interactive theorem proving,
both for formalization of mathematics and for verification of computer
- Project home page for auto2:
- Formalization of the fundamental group in untyped set theory using auto2.
- Automation of separation logic using auto2.
- AUTO2, a saturation-based heuristic prover for higher-order logic.
During graduate school, I did research in low dimensional topology, in
particular Heegaard Floer homology.