A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (Abstract)
A general framework for synthesizing efficient programs, using tools such as higher-order unification (henceforth HOU), has been developed and holds promise for encapsulating an otherwise diverse, and often ad hoc, range of transformation techniques. A prototype system has been implemented. Proof plans — formal outlines of constructive proofs — are used to control the (automatic) synthesis of the efficient programs from standard definitional equations [1,6,5]. Programs are specified in the standard equational form within the logic of the OYSTER proof refinement system. The construction of the improved functions is automatically controlled using the CLAM proof planner .
Unable to display preview. Download preview PDF.
- A. Bundy, A. Stevens, F. van Harmelen, A. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. Research Paper 567, Dept. of Artificial Intelligence, Edinburgh, 1991. In the Journal of Artificial Intelligence.Google Scholar
- A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. Research Paper 507, Dept. of Artificial Intelligence, Edinburgh, 1990. Appeared in the proceedings of CADE-10.Google Scholar
- H.B. Curry and R. Feys. Combinatory Logic. North-Holland, 1958.Google Scholar
- W.A. Howard. The formulae-as-types notion of construction. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980.Google Scholar
- P. Madden, I. Green, and A. Bundy. A General Technique for Optimizing Programs by using Proof Plans. Technical Report in preperation, Dept. of Artificial Intelligence, University of Edinburgh, 1993.Google Scholar
- P. Madden, J. Hesketh, I. Green, and A. Bundy. A general technique for automatically optimizing programs through the use of proof plans. Research Paper 608, Dept. of Artificial Intelligence, Edinburgh, 1993.Google Scholar