Towards Formal Proof Script Refactoring

Iain Whiteside, David Aspinall, Lucas Dixon, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We propose proof script refactorings as a robust tool for constructing, restructuring, and maintaining formal proof developments. We argue that a formal approach is vital, and illustrate by defining and proving correct a number of valuable refactorings in a simplified proof script and declarative proof language of our own design.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings
EditorsJames Davenport, William Farmer, Josef Urban, Florian Rabe
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-642-22673-1
ISBN (Print)978-3-642-22672-4
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Cite this