Mathematics and Computation

A blog about mathematics for computers

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.

Comments

James McKinna

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

Andrej Bauer

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.

James McKinna

Got the fixed version now. Thanks for being so efficient.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.