Towards a formal theory of program construction.

Christoph Kreitz.

Revue d' intelligence artificielle 4(3):53-79, 1990.


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.

Back to overview of papers

Bibtex Entry

@Article{ar:Kreitz90a, author = "Christoph Kreitz", title = "Towards a formal theory of program construction", journal = "Revue d' intelligence artificielle", year = 1990, volume = "4", number = "3", pages = "53--79" }