Formal Mathematics for Verifiably Correct Program Synthesis.


Christoph Kreitz.  
Journal of the Interest Group in Pure and Applied Logics (J.IGPL), 4(1):7594, 1996. 

Abstract 

We describe a formalization of the metamathematics of programming in a
higherorder 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 = "7594" } 