Formal Mathematics for Verifiably Correct Program Synthesis.
Christoph Kreitz.
Journal of the Interest Group in Pure and Applied Logics (J.IGPL), 4(1):75-94, 1996.
Abstract
	We describe a formalization of the meta-mathematics of programming in a higher-order logical calculus as a means to create verifiably correct implementations of program synthesis tools. Using reflected notions of programming concepts we can specify the actions of synthesis methods within the object language of the calculus and prove formal theorems about their behavior. The theorems serve as derived inference rules implementing the kernel of these methods in a flexible, safe, efficient and comprehensible way. We demonstrate the advantages of using formal mathematics in support of program development systems through an example in which we formalize a strategy for deriving global search algorithms from formal specifications.

			Back to overview of papers
Bibtex Entry
	@Article{ar:Kreitz96a, author = "Christoph Kreitz", title = "Formal Mathematics for Verifiably Correct Program Synthesis", journal = "Journal of the IGPL", year = 1996, volume = 4, number = 1, pages = "75--94" }