RZ: a tool for bringing constructive and computable mathematics closer to programming practice

With Chris Stone.

Abstract:
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.

Download paper:

Download slides: cie2007-slides.pdf

Download source code from RZ web page.

3 thoughts on “RZ: a tool for bringing constructive and computable mathematics closer to programming practice

  1. The slides appear to have been corrupted, or so says my Acrobat Reader (Version 8).

  2. 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.

Leave a Reply

Your email address will not be published. Required fields are marked *

− 1 = 1

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>