Towards formal proof script refactoring

Iain Whiteside, David Aspinall, Lucas Dixon, Gudmund Grov

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

15 Citations (Scopus)

Abstract

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 publication Proceedings of the18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011
EditorsJames H. Davenport, William M. Farmer, Josef Urban, Florian Rabe
Pages260-275
Number of pages16
Volume6824
DOIs
Publication statusPublished - 2011
EventIntelligent Computer Mathematics 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011 - Bertinoro, Italy, Italy
Duration: 18 Jul 201123 Jul 2011

Publication series

NameLecture Notes in Computer Science: Lecture Notes in Artificial Intelligence
PublisherSpringer Berlin
Volume6824
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceIntelligent Computer Mathematics 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011
CountryItaly
CityBertinoro, Italy,
Period18/07/1123/07/11

Cite this

Whiteside, I., Aspinall, D., Dixon, L., & Grov, G. (2011). Towards formal proof script refactoring. In J. H. Davenport, W. M. Farmer, J. Urban, & F. Rabe (Eds.), Intelligent Computer Mathematics: Proceedings of the18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011 (Vol. 6824, pp. 260-275). (Lecture Notes in Computer Science: Lecture Notes in Artificial Intelligence; Vol. 6824). https://doi.org/10.1007/978-3-642-22673-1_18