RZ: a tool for bringing constructive and computable mathematics closer to programming practice
- 21 January 2007
- Publications, RZ, Talks
With Chris Stone.
Realizability theory is not only a fundamental tool in logic and computability, but also has direct application to the design and implementation of programs: it can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between the worlds of constructive mathematics and programming. By using the realizability interpretation of constructive mathematics, RZ translates specifications in constructive logic into annotated interface code in Objective Caml. The system supports a rich input language allowing descriptions of complex mathematical structures. RZ does not extract code from proofs, but allows any implementation method, from handwritten code to code extracted from proofs by other tools.
Presented at Computablity in Europe 2007.
- Long version: cie-long.pdf (January 29, 2007)
- Short version: cie-short.pdf (January 29, 2007)
Download slides: cie2007-slides.pdf
Download source code from RZ web page.
The slides appear to have been corrupted, or so says my Acrobat Reader (Version 8).
Thank you for spotting this. I fixed it. If you are still getting a corrupted file, it is because your browser is holding te old version in cache.
Got the fixed version now. Thanks for being so efficient.