School of Computing

A Certified Refactoring Engine

Nik Sultana and Simon Thompson

In P. Achten, P. Koopman, and M. T. Moraz�n, editors, Draft Proceedings of the Ninth Symposium on Trends in Functional Programming (TFP), pages 182-196, May 2008.

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.

Download publication 105 kbytes (PDF)

Bibtex Record

@inproceedings{2778,
author = {Nik Sultana and Simon Thompson},
title = {{A Certified Refactoring Engine}},
month = {May},
year = {2008},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2008/2778},
    publication_type = {inproceedings},
    submission_id = {635_1213200574},
    booktitle = {Draft Proceedings of the Ninth Symposium on Trends in Functional Programming (TFP)},
    editor = { P. Achten and  P. Koopman and M. T. Moraz�n},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014