A Certified Refactoring Engine

Sultana, Nik and Thompson, Simon (2008) A Certified Refactoring Engine. In: Draft Proceedings of the Ninth Symposium on Trends in Functional Programming (TFP). (Full text available)

Download (108kB)


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.

Item Type: Conference or workshop item (UNSPECIFIED)
Uncontrolled keywords: refactoring, verification, Isabelle, program extraction, proof
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 29 Mar 2010 12:09
Last Modified: 06 Sep 2011 04:51
Resource URI: https://kar.kent.ac.uk/id/eprint/23987 (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year