MRG home page · Research · Publications · Projects · Software · People

Proof Engineering: Refactoring Proof

This project aims to develop refactoring techniques for proof scripts in proof assistants such as Isabelle and Coq .

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".
Mathematical Reasoning Group, Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland
Tel: +44 (0)131 650 2733      Fax: +44 (0)131 650 6899
Please send corrections and suggestions for this page to the DReaM Support Team
Unless explicitly stated otherwise all material on this web site is copyright © The University of Edinburgh.