I'm currently working with Emily First, Alex Sanchez-Stern, Timothy Zhou, Zhanna Kaufman, and Yuriy Brun on improving neural tactic prediction models for Coq by enriching them with missing syntactic and semantic information. The goal is use these tactic prediction models to improve performance of tools for both proof synthesis and repair. It's a lot of fun!
I'm also working with Cosmo Viola on extending proof repair tools to handle relations more general than equivalences. This is much more on the type theory side of things. I'm excited to see how powerful we can make these tools.
With Chris Lam, Audrey Seo, Dan Grossman, and Zach Tatlock, I'm working on using automation based on proof repair to automatically compile proofs about programs alongside the programs themselves---without requiring a full formal proof of compiler correctness!
With Louis Castricato, Ryan Teehan, and Shahbuland Matiana, I'm working on collecting a large pair programming dataset with atomic edits, rationales, and execution data. This is part of EleutherAI, a super cool artificial intelligence collective. So literally anyone---yes, you---can join this project if they'd like. We're in
#constrastive on Discord!
I have a few other (perhaps too many) budding projects on topics like 1) formally verified secure hardware systems, and 2) the strangely rich intersection of cubical type theory and machine learning. I am always happy to hear what students want to work on!