Skip to main content

A Certified Refactoring Engine

Sultana, Nik, Thompson, Simon (2008) A Certified Refactoring Engine. In: Achten, P. and Koopman, P. and Morazán, M.T., eds. Draft Proceedings of the Ninth Symposium on Trends in Functional Programming (TFP). . (KAR id:23987)

PDF
Language: English
Download (157kB) Preview
[thumbnail of CertifiedThompson.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format

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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 29 Mar 2010 12:09 UTC
Last Modified: 16 Feb 2021 12:34 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/23987 (The current URI for this page, for reference purposes)
Thompson, Simon: https://orcid.org/0000-0002-2350-301X
  • Depositors only (login required):

Downloads

Downloads per month over past year