I am exploring a number of exciting topics right now, all with an underlying theme of proof engineering, and especially proof automation. In addition to my wonderful lab, I have wonderful collaborators at UW, UMass Amherst, Google Research, and Stanford with whom I'm super fortunate to explore these topics:
Proof Repair: How can we extend proof repair to make it more powerful and practical, so that it reaches proof engineers of all levels of expertise, across many different domains? I have four collaborations exploring this question, with techniques ranging from dependent type theory and proof term transformations to machine learning.
Machine Learning for Proofs: What can machine learning do for proof engineers, and how can this advance the state of the art in machine learning? What would it take to make machine learning tools for proofs much more practical---to infer and apply deep semantic relations, and to handle the tasks most difficult for proof engineers? This is an exciting and hot topic I'm having a lot of fun exploring with many collaborators.
Proof Engineering: How can we advance the state of the art in proof engineering, and use it to drive the development of large, secure, and robust verified software and hardware systems? I have two collaborations exploring new domains and new kinds of proof engineering, looking at everything from compilation of proofs to verification of critical security properties of hardware.