Show simple item record

dc.contributor.advisorDixon, Lucas
dc.contributor.advisorGrov, Gudmund
dc.contributor.advisorAspinall, David
dc.contributor.authorWhiteside, Iain Johnston
dc.date.accessioned2013-10-22T13:56:14Z
dc.date.available2013-10-22T13:56:14Z
dc.date.issued2013-11-28
dc.identifier.urihttp://hdl.handle.net/1842/7970
dc.description.abstractRefactoring is an important Software Engineering technique for improving the structure of a program after it has been written. Refactorings improve the maintainability, readability, and design of a program without affecting its external behaviour. In analogy, this thesis introduces proof refactoring to make structured, semantics preserving changes to the proof documents constructed by interactive theorem provers as part of a formal proof development. In order to formally study proof refactoring, the first part of this thesis constructs a proof language framework, Hiscript. The Hiscript framework consists of a procedural tactic language, a declarative proof language, and a modular theory language. Each level of this framework is equipped with a formal semantics based on a hierarchical notion of proof trees. Furthermore, this framework is generic as it does not prescribe an underlying logical kernel. This part contributes an investigation of semantics for formal proof documents, which is proved to construct valid proofs. Moreover, in analogy with type-checking, static well-formedness checks of proof documents are separated from evaluation of the proof. Furthermore, a subset of the SSReflect language for Coq, called eSSence, is also encoded using hierarchical proofs. Both Hiscript and eSSence are shown to have language elements with a natural hierarchical representation. In the second part, proof refactoring is put on a formal footing with a definition using the Hiscript framework. Over thirty refactorings are formally specified and proved to preserve the semantics in a precise way for the Hiscript language, including traditional structural refactorings, such as rename item, and proof specific refactorings such as backwards proof to forwards proof and declarative to procedural. Finally, a concrete, generic refactoring framework, called Polar, is introduced. Polar is based on graph rewriting and has been implemented with over ten refactorings and for two proof languages, including Hiscript. Finally, the third part concludes with some wishes for the future.en_US
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en_US
dc.language.isoenen_US
dc.publisherThe University of Edinburghen_US
dc.relation.hasversionWhiteside, I., Aspinall, D., Dixon, L., and Grov, G. (2011). Towards formal proof script refactoring. In Davenport, J. H., Farmer, W. M., Urban, J., and Rabe, F., editors, Calculemus/MKM, volume 6824 of Lecture Notes in Computer Science, pages 260–275. Springer.en_US
dc.relation.hasversionWhiteside, I., Aspinall, D., and Grov, G. (2012). An essence of SSReflect. In Jeuring et al. (2012), pages 186–201.en_US
dc.subjectrefactoringen_US
dc.subjectHiscripten_US
dc.subjectformal semanticsen_US
dc.subjectproof treesen_US
dc.titleRefactoring proofsen_US
dc.typeThesis or Dissertationen_US
dc.type.qualificationlevelDoctoralen_US
dc.type.qualificationnamePhD Doctor of Philosophyen_US


Files in this item

This item appears in the following Collection(s)

Show simple item record