Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #777 | |
|---|---|
| Title: | Automating the Synthesis of Functional Programs in Constructive Type Theory |
| Authors: | Smaill,AD; Green,I |
| Date: | Dec 1995 |
| Presented: | Submitted to IJCAI |
| Keywords: | |
| Abstract: | The task of constructing programs can be treated as a task of finding proofs in an appropriate logic. For recursive programs, the corresponding logic includes appropriate induction principles. We describe a system that automates program synthesis via theorem proving in this way, building on control strategies developed for verification proofs using proof plans. This involves some extensions to the planning system. The resultant system automates an approach to programming where program development and correctness proof proceed hand in hand, as advocated by Gries. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}