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 [2].
This research was supported by SERC grant GR/H/23610 and a SERC Postdoctoral Fellowship to the first author.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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.
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.
H.B. Curry and R. Feys. Combinatory Logic. North-Holland, 1958.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 British Computer Society
About this paper
Cite this paper
Madden, P., Hesketh, J., Green, I., Bundy, A. (1994). A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (Abstract). In: Deville, Y. (eds) Logic Program Synthesis and Transformation. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3234-9_6
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3234-9_6
Publisher Name: Springer, London
Print ISBN: 978-3-540-19864-2
Online ISBN: 978-1-4471-3234-9
eBook Packages: Springer Book Archive