The Representation of Program Synthesis in Higher Order Logic

8 years 10 months ago
The Representation of Program Synthesis in Higher Order Logic
ue 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 t 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. T...
Christoph Kreitz
Added 11 Aug 2010
Updated 11 Aug 2010
Type Conference
Year 1990
Where KI
Authors Christoph Kreitz
Comments (0)