Previous: TR 94-05 Next: TR 94-08


Intellektik: Technical report 94-07

A Foundation for Verified Software Development Systems

C. Kreitz

We describe a formalization of the meta-mathematics of programming in a higher-order calculus as a means to create verifiably correct implementations of program synthesis tools. Formal definitions and lemmata are used to raise the level of abstraction in formal reasoning to one comprehensible for programmers. Formal meta-theorems make explicit the semantic knowledge contained in program derivation methods and serve as kernel of derived inference rules implementing these methods. By an example formalization of a strategy deriving global search algorithms we demonstrate the advantages of combining formal mathematics with an interactive theorem proving environment to develop powerful, flexible, and reliable systems for knowledge-based software development. We describe a formalization of the meta-mathematics of programming in a higher-order calculus as a means to create verifiably correct implementations of program synthesis tools. Formal definitions and lemmata are used to raise the level of abstraction in formal reasoning to one comprehensible for programmers. Formal meta-theorems make explicit the semantic knowledge contained in program derivation methods and serve as kernel of derived inference rules implementing these methods. By an example formalization of a strategy deriving global search algorithms we demonstrate the advantages of combining formal mathematics with an interactive theorem proving environment to develop powerful, flexible, and reliable systems for knowledge-based software development.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry