I have now moved to the Institute of Software, Chinese Academy of
Sciences. The new (and updated) website is
Chair for Logic and Verification
Technical University of Munich
I am working on automation techniques in interactive theorem proving,
both for formalization of mathematics and for verification of computer
Project at github
- (with Maximilian P. L. Haslbeck) Verifying asymptotic time complexity of imperative programs in Isabelle.
- Efficient verification of imperative programs using auto2.
- Formalization of the fundamental group in untyped set theory using auto2.
- AUTO2, a saturation-based heuristic prover for higher-order logic.
- Proof automation in set theory. Conference in honour of Thomas C. Hales on the occasion of his 60th birthday.
During graduate school, I did research in low dimensional topology, in
particular Heegaard Floer homology.