Knowledge-Based Software Engineering Conference (1995)

Boston, Massachusetts

Nov. 12, 1995 to Nov. 15, 1995

ISSN: 1068-3062

ISBN: 0-8186-7204-8

pp: 166

J. Richardson , Dept. of Artificial Intelligence, Edinburgh Univ., UK

ABSTRACT

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

CITATION

J. Richardson,
"Automating changes of data type in functional programs",

*Knowledge-Based Software Engineering Conference*, vol. 00, no. , pp. 166, 1995, doi:10.1109/KBSE.1995.490132