Sultana, Nik and Thompson, Simon
A Certified Refactoring Engine.
In: Draft Proceedings of the Ninth Symposium on Trends in Functional Programming (TFP).
(Full text available)
The paper surveys how software tools such as refactoring systems can be validated, and introduces a new mechanism, namely the extraction of a refactoring engine for a functional programming language from an Isabelle/HOL theory in which it is verified. This research is a first step in a programme to construct certified programming tools from verified theories. We also provide some empirical evidence of how refactoring can be of significant benefit in reshaping automatically-generated program code for use in larger systems.
- Depositors only (login required):