The representation of program synthesis in higher order logic.


Christoph Kreitz.  
In H. Marburger, ed., 14th German Workshop on Artificial Intelligence, Informatik Fachberichte 251, pp. 171180, Springer Verlag, 1990. 

Abstract 

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 metamathematics 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. 

Also presented at University of Kaiserslautern, Kaiserslautern, Germany, December 1990. 
Paper is available in
postscript and pdf format 
Slides of the conference presentation are available in compressed postscript and pdf format  
Bibtex Entry 
Back to overview of papers 

@InProceedings{inp:Kreitz90a, author = "Christoph Kreitz", title = "The Representation of Program Synthesis in Higher Order Logic", booktitle = "GWAI90  14$^{th}$ German Workshop on Artificial Intelligence", year = 1990, editor = "H. Marburger", pages = "171180", series = "Informatik Fachberichte", volume = 251, publisher = "Springer Verlag" } 