The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #767

Title:Automating Changes of Data Type in Functional Programs
Date:Aug 1995
Presented:Accepted for presentation at KBSE-95, November 1995
Abstract:In this paper I present an automatic technique for transforming a program by changing the data types in that program to ones which are more appropriate for the task. Programs are synthesised by providing modified synthesis theorems in the proofs-as-programs paradigm. the transformation can be verified in the logic of type theory. Transformations are motivated by the presence of subexpressions in the synthesised program. A library of data type changes is maintained, indexed by the motivating subexpressions. These transformations are extended from the motivating expressions to cover as much of the program as possible. I describe the general pattern of the revised synthesis proof, and show how such a proof can be guided by difference matching followed by rippling.

[Search These Pages] [DAI Home Page] [Comment]