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

- 21 January 2007
- Publications, RZ, Talks

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:**

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

##### Post a comment:

`$⋯$`

for inline and `$$⋯$$`

for display LaTeX formulas,
and `<pre>⋯</pre>`

for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.
## Comments

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.