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 development of 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 Intuitionistic Type 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