@inproceedings{dfdc05a5c3154cfaa8638d0e4da9933e,

title = "Towards formal proof script refactoring",

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

author = "Iain Whiteside and David Aspinall and Lucas Dixon and Gudmund Grov",

year = "2011",

doi = "10.1007/978-3-642-22673-1_18",

language = "English",

isbn = "978-3-642-22672-4",

volume = "6824",

series = "Lecture Notes in Computer Science: Lecture Notes in Artificial Intelligence",

publisher = "Springer Berlin",

pages = "260--275",

editor = "Davenport, {James H. } and Farmer, {William M. } and Urban, {Josef } and Rabe, {Florian }",

booktitle = "Intelligent Computer Mathematics",

note = "Intelligent Computer Mathematics 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011 ; Conference date: 18-07-2011 Through 23-07-2011",

}