Previous: TR 93-12 Next: TR 93-17

Intellektik: Technical report 93-13

Formal Mathematics for Verifiably Correct Program Synthesis

Christoph Kreitz

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.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry