Abstract: Coq proofs are unlike pen-and-paper proofs in one key way: in Coq, we write tactics that describe how to advance the proof, but we leave the tedium of computing the resulting proof states (goals) to the machine. Advanced user interfaces display these proof goals in real time (like Proof General, jsCoq, and CoqIDE) and make it relatively easy to read proof scripts.

Unfortunately, these interactive interfaces are not universally applicable: they don’t work in printed materials, email, or on simple websites, for example. As a result, most written material on Coq either shows very few proofs, or includes manual copies of goals and responses computed by Coq — a tedious and error-prone process.

I recently released Alectryon, an automated proof-recorder and literate-programming toolkit for Coq (work is in progress to support EasyCrypt and Lean). This talk will introduce Alectryon, describe some recent extensions to it aimed at supporting larger and more complex Coq developments, demonstrate how to use it for your own Coq code, and serve as a call to action to improve the state of the art in the documentation and distribution of Coq proofs.

I’m a senior applied scientist at Amazon AWS, soon to join EPFL as an assistant professor. Previously, I was a PhD candidate at MIT with Adam Chlipala. My research focuses on programming languages, compilers, and formal verification; my broader interests include systems engineering, hardware design languages, security, performance engineering, databases, and type theory. I work on end-to-end verified compilation pipelines from high-level specifications to assembly language, verified compilers and fast simulation for rule-based hardware design languages with EHRs, and Coq tooling.