My current focus lies on improving the support for the theory of arrays in the Vampire prover. I am particularly interested in proving conjectures of the form "There exists an array with the following properties: ...".
Previously I was working on TLAPM, an interactive theorem prover for the temporal logic TLA+.
A main motivation for my current activities comes from my work on CERESĪ, a cut-elimination method for higher-order proofs using automated theorem provers. For my PhD thesis, I used the method to extract function definitions from proofs in higher-order logic. All experiments were done using the GAPT framework for proof theory to which I am still contributing from time to time.
If you are interested in hard problems for automated higher-order provers, you can find a collection here.