Building systems in proof assistants is challenging for many reasons. Such systems must tolerate changes gracefully: definitions may be optimized for performance, new theorems may be added, and the proof assistant itself may change how tactics work. Proof assistants are also highly expressive; engineers must ensure that their specifications do not accidentally allow for undesirable behavior. Furthermore, large-scale developments often depend on good tactic performance, requiring developers to reason about low-level performance costs.
To help address these challenges, the Proof Engineering (PE) project is collecting best practices and building techniques and tools for developing large systems in the demanding and foundational context of proof assistants.
Nov 2017 Papers in ASE 2017 and CPP 2018.
May 2017 Site goes live.
Proof Engineering is an international collaboration between researchers at the University of Washington (UW), University College London (UCL), the University of Illinois at Urbana-Champaign (UIUC), the University of Texas at Austin (UT), and Cornell University (CU). Many volunteers have helped out on PE projects; we're very grateful for their contributions! Folks currently working on PE include: