Dependable performance

Improving the efficiency of programs through transformation is an important and active area of research. Within the Parallel SML compiler project² at Heriot-Watt, we are using transformation techniques to increase the opportunities for exploiting parallelism. The transformations we are interested in are those which introduce higher-order functions (HOFs), i.e. functions which take functions as arguments. HOFs are closely related to generic parallel constructs and consequently are amenable to parallelism. We are investigating the use of the proof planning framework to verify the correctness of the transformations used within the Parallel SML compiler. In addition, we aim to dynamically synthesise new transformations on demand, using proof plans to constrain the search.