AESOP home

Publications

The mechanical transformation of data types

Peter G. Harrison, Hessam Khoshnevisan

Journal Article
The Computer Journal
Volume 35
Issue 2
pp.138–147
March, 1992
Oxford Journals
DOI 10.1093/comjnl/35.2.138
Abstract

The efficient implementation of abstract data types and all functions that manipulate them would permit application-oriented solutions to be developed without having to take undue account of executional properties. The synthesis of efficient concrete types and functions forms the basis of the present paper, which appeals to a theory of inverse functions for additional axioms to augment those of a first-order functional algebra. These axioms are then applied in the simplification of the combinator-expressions arising in the synthesis of the functions between the concrete types. We also show how the abstraction function itself may be deduced in certain situations where it is required to optimise particular operations on an abstract type. In addition to possessing rigorous mathematical foundations, the function-level axioms are more generally applicable than previous approaches to this problem, and induce a more mechanisable rewrite-based transformation system.

Information from pubs.doc.ic.ac.uk/data-type-transformation.