A Foundation for Verified Software Development Systems.


Christoph Kreitz.  
Forschungsbericht AIDA9407, Technische Hochschule Darmstadt, FG Intellektik, 1994. 

Abstract 

We describe a formalization of the metamathematics of programming in a
higherorder 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 metatheorems 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 knowledgebased
software development.

Back to overview of papers 

Bibtex Entry 

@TechReport{tr:Kreitz94a, author = "Christoph Kreitz", title = "A Foundation for Verified Software Development Systems", institution = "TU Darmstadt, FG Intellektik", year = 1994, month = "August", type = "Forschungsbericht", number = "AIDA9407" } 