Intellektik: Technical report 90-07
The representation of Program Synthesis in Higher Order Logic
Systems built for automated program construction aim at the formalization of the
programming process in order to produce better software.
Their implementations, however, suffer from problems similar to those they
are intended to solve. Due to a lack of abstraction in the formalization of
deductive mechanisms involved in programming reasoning tools for the developmentof program synthesizers are not yet available. For that, systems capable of
formal reasoning about both programs and programming methods are needed.
In this paper we develop principles of a formal theory on reasoning about
programs and program construction within a unified higher order framework.
By an exemplified formalization of principal approaches to program
synthesis we will show that a higher degree of abstraction leads to clearer
insights into the meta-mathematics of program construction. Ridding the
representation of deductive methods from superfluous context also results in
simpler, sometimes almost trivial, proofs. Simplicity is one of the most
important features of the formal theory and quite valuable if one considers the
wide range of intended applications.
We present the theory in a highly formalized form built on top of IntuitionisticType Theory. This allows us to straightforwardly implemented the concepts
developed here with a proof system for Type Theory and derive verified
implementations of deductive mechanisms from mechanically proven theorems.