The University of Edinburgh -
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
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.

[Search These Pages] [DAI Home Page] [Comment]