It does not bode well to have a website titled “notes on PhD research” without actually talking about the research. I will try to provide a glimpse into what I have been up to in my PhD—and what I am trying to achieve at the end of it.
My research interests lie in formal methods, software verification, and—especially—theorem proving as part of the formal system development. The state of art in theorem proving of “industrial” (as opposed to mathematical) proofs is that still quite significant effort is spent in interactive proof. In AI4FM project we aim to increase automation here by learning from an expert doing proof and then completing similar proofs automatically.
My PhD research is most concerned with capturing and understanding the interactive proof. I am investigating how to capture expert’s ideas as a high-level proof process. The proof process data with sufficient information could then serve to extract reusable strategies and eventually replay them on similar proofs.
I am developing some of the ideas as a generic ProofProcess framework. It serves as the infrastructure to capture and infer the proof process for different theorem provers. The system links closely with proof assistants such as Isabelle or Z/EVES (via new prover IDEs/tools).
Further details on the PhD are available in the new dedicated page for my research. Also check out the updated About page for the bigger picture.