This Article 
 Bibliographic References 
 Add to: 
The 10th Knowledge-Based Software Engineering Conference
Automating changes of data type in functional programs
Boston, Massachusetts
November 12-November 15
ISBN: 0-8186-7204-8
J. Richardson, Dept. of Artificial Intelligence, Edinburgh Univ., UK
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 proving 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.
Index Terms:
data structures; functional programming; theorem proving; program verification; type theory; programming theory; software libraries; libraries; automatic technique; automated data type changes; functional programs; program transformation; program synthesis; modified synthesis theorem proving; proofs-as-programs paradigm; type theory logic; verification; subexpressions; data type change library; revised synthesis proof; difference matching; rippling
J. Richardson, "Automating changes of data type in functional programs," kbse, pp.166, The 10th Knowledge-Based Software Engineering Conference, 1995
Usage of this product signifies your acceptance of the Terms of Use.