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)

PDF
Download (108kB)
[img]
Preview

Abstract

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: http://kar.kent.ac.uk/id/eprint/23987 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year