Interactive theorem provers have important applications in software and hardware verification and mechanising mathematical proofs. There have been some large proof developments, such as Gonthier's formalisation of the proof of the Four Colour Theorem using the Coq proof assistant; however, large developments are more difficult to create and manage due to the lack of tool support. In contrast, modern programming language IDEs have powerful debugging features, 'wizards' for class templates, automated code refactoring and content assistance. All these features have similar applications within a proof development environment, but very few have been implemented.
In software engineering, a refactoring is a semantics preserving transformation on a body of code to improve design, structure or readability.
For proof refactoring, the concept of semantics preservation is subtle: a rename
refactoring may be guaranteed to preserve proofs and statements, but a change type
refactoring will inherently change what is being proved. Reliable refactorings like rename
should be routine, but refactorings should also be debuggable (for more complex transformations).
The people involved in this project are:
This project is sponsored by Microsoft Research grant "Proof Engineering: Refactoring Proof".