Refactoring SASyLF Proofs

Abstract

Refactoring is a common practice undertaken by software developers that is used to improve the quality of existing code. Originally done by hand, several automated refactorings have been introduced over the years, saving both time and effort expended by the developer. Proof engineering, on the other hand, is a more recent concept which has not advanced as quickly over the years, thus they do not have similar tools to be able to make similar changes automatically. Since proof assistants resemble programming languages in many regards, a similar practice may be applied.Thus, the main idea behind this thesis is introduced. The topic of refactoring is discussed, and how it can be applied to proof assistants as well as for programming languages. The framework of the proof assistant SASyLF is also introduced, including a description of its different components and its syntax. Additionally, some related work regarding proof refactoring is mentioned.