NSF Postdoctoral Fellow

Department of Mathematics

Massachusetts Institute of Technology

bzhan@mit.edu

I am working on automation techniques in interactive theorem proving, both for formalization of mathematics and for verification of computer programs.

- Project home page for auto2: https://github.com/bzhan/auto2
- Formalization of the fundamental group in untyped set theory using auto2.
*ITP 2017*paper - Automation of separation logic using auto2.
*preprint*arXiv - AUTO2, a saturation-based heuristic prover for higher-order logic.
*ITP 2016*arXiv slides

- Python code for computations in bordered Floer homology: https://github.com/bzhan/bfh_python
- Combinatorial proofs in bordered Heegaard Floer homology.
*Algebr. Geom. Topol.*16 (2016) 2571-2636 arXiv published version - Explicit Koszul-dualizing bimodules in bordered Heegaard Floer homology.
*Algebr. Geom. Topol.*16 (2016) 231-266 arXiv published version