© University of Kent - Contact | Feedback | Legal | FOI | Cookies
A Certified Refactoring Engine
Nik Sultana and Simon Thompson
In P. Achten, P. Koopman, and M. T. Morazn, 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. Morazn}, }