Higher order function synthesis through proof planning

The close association between higher order functions and algorithmic skeletons is a promising source of automatic parallelisation of programs. An approach to automatically synthesizing higher order functions from functional programs through proof planning is presented Our work has been conducted within the context of a parallelising compiler for SML, with the objective of exploiting parallelism latent in potential higher order function use in programs.