Preview
Unable to display preview. Download preview PDF.
References
R. Aubin. Some generalization heuristics in proofs by induction. In G. Huet and G. Kahn, editors, Actes du Colloque Construction: Amélioration et vérification de Programmes. Institut de recherche d'informatique et d'automatique, 1975.
A. Bundy, F. van Harmelen, J. Hesketh, and A. Smaill. Experiments with proof plans for induction. Journal of Automated Reasoning, 7:303–324, 1991.
A. Bundy, van Harmelen. F., C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag, 1990. Lecture Notes in AI No.449.
R.M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the Association for Computing Machinery, 24(1):44–67, 1977.
W. N. Chin. Automatic Methods for Program Transformation. PhD thesis, University of London (Imperial College), 1990.
N. H. Cohen. Eliminating redundant recursive calls. volume 5 No. 3, pages 265–299. 1983.
H.B. Curry and R. Feys. Combinatory Logic. North-Holland, 1958.
J. Darlington. A Semantic Approach to Automatic Program Improvement. PhD thesis, Dept. of Artificial Intelligence, Edinburgh, 1972.
C. A. Goad. Computational uses of the manipulation of formal proofs. Technical report, Stanford University, 1980. STAN-CS-80-819.
C. A. Goad. Proofs as descriptions of computation. In Lecture Notes in Computer Science. Academic Press, 1980.
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. The specialization and transformation of. constructive existence proofs. In N.S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence. Morgan Kaufmann, 1989. Also available from Edinburgh as DAI Research Paper 416.
P. Madden. Automated Program Transformation Through Proof Transformation. PhD thesis, University of Edinburgh, 1991.
Per Martin-Löf. Constructive mathematics and computer programming. In 6th International Congress for Logic, Methodology and Philosophy of Science, pages 153–175, Hanover, August 1979. North Holland, Amsterdam. 1982.
A. Pettorossi. A powerful strategy for deriving programs by transformation. In ACM Lisp and Functional Programming Conference, pages 405–426, 1984.
H. Tamaki and T. Sato. A transformation system for logic programs that preserves equivalence. Technical Report TR-018, ICOT, 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Madden, P. (1992). Automatic program optimization through proof transformation. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_183
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_183
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive