Towards automatic program synthesis

Placeholder Show Content


An elementary outline of the theorem-proving approach to automatic program synthesis is given, without dwelling on technical details. The method is illustrated by the automatic construction of both recursive and iterative programs operating on natural numbers, lists, and trees. In order to construct a program satisfying certain specifications, a theorem induced by those specifications is proved, and the desired program is extracted from the proof. The same technique is applied to transform recursively defined functions into iterative programs, frequently with a major gain in efficiency. It is emphasized that in order to construct a program with loops or with recursion, the principle of mathematical induction must be applied. The relation between the version of the induction rule used and the form of the program constructed is explored in some detail.


Type of resource text
Form technical reports
Extent 1 text file
Place Stanford (Calif.)
Date created July 1, 1970
Language English
Digital origin reformatted digital


Author Manna, Zohar


Subject Stanford University. Computer Science Department
Subject Computer science
Genre Technical reports

Bibliographic information

Finding Aid
Technical Report # CS-TR-1970-174
Location 3840/2
Repository Stanford University. Libraries. Department of Special Collections and University Archives

Access conditions

Use and reproduction
The materials are open for research use and may be used freely for non-commercial purposes with an attribution. For commercial permission requests, please contact the Stanford University Archives (


Stanford University, Department of Computer Science, Technical Reports

View other items in this collection in SearchWorks

Stanford Artificial Intelligence Laboratory records, 1963-2009

View other items in this collection in SearchWorks

Also listed in

Loading usage metrics...