Discovering applications of higher order functions through proof planning

Andrew Cook, Andrew Ireland, Gregory John Michaelson, Norman Scaife

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)


The close association between higher order functions (HOFs) and algorithmic skeletons is a promising source of automatic parallelisation of programs. A theorem proving approach to discovering HOFs in functional programs is presented. Our starting point is proof planning, an automated theorem proving technique in which high-level proof plans are used to guide proof search. We use proof planning to identify provably correct transformation rules that introduce HOFs. The approach has been implemented in the ? Clam proof planner and tested on a range of examples. The work was conducted within the context of a parallelising compiler for Standard ML. BCS © 2005.

Original languageEnglish
Pages (from-to)38-57
Number of pages20
JournalFormal Aspects of Computing
Issue number1
Publication statusPublished - May 2005


Dive into the research topics of 'Discovering applications of higher order functions through proof planning'. Together they form a unique fingerprint.

Cite this