Motivation
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.
Refactoring
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).
People
The people involved in this project are:
Links
Thanks
This project is sponsored by Microsoft Research grant "Proof Engineering: Refactoring Proof".
