Previous: TR 89-06 Next: TR 90-07

Intellektik: Technical report 90-01

Towards a formal theory of program construction

Christoph Kreitz

A unified framework for formal reasoning about programs and deductive mechanisms involved in programming is developed. Within it principal approaches to program synthesis are formally investigated. We will show that a high degree of abstraction opens a way to combine their strengths, simplifies formal proofs, and leads to clearer insights into the meta-mathematics of program construction. All definitions and theorems are presented completely formal which allows to straightforwardly implement them with a proof system for the underlying calculus and derive verified implementations of programming methods from them.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry: