Intellektik: Technical report 93-13
Formal Mathematics for Verifiably Correct Program Synthesis
We describe a formalization of the meta-mathematics of
programming as a means to implement verifiably correct tools for
program synthesis. We demonstrate the advantages of using formal
mathematics as support for AI-techniques by an example formalization
of a strategy deriving global search algorithms from specifications.