A Foundation for Verified Software Development Systems.
Christoph Kreitz.
Forschungsbericht AIDA-94-07, Technische Hochschule Darmstadt, FG Intellektik, 1994.
Abstract
	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.

			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 = "AIDA--94--07" }