### 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".