Home

RZ for Constructive Mathematics in Programming

RZ for Constructive Mathematics in Programming by Chris Stone and Andrej Bauer.

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.

I haven't read the paper yet, but the abstract reminded me of PADS.

By Jim Apple at 2007-02-03 21:19 | DSL | Semantics | Theory | Type Theory | other blogs | 6222 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

[Style]

Style issues: (1) The whole abstract is a link. That's too much. (2) You should assign a department to homepage items (if you don't, alas, it defaults to the Admin department).

By Ehud Lamm at Sat, 2007-02-03 21:24 | login or register to post comments

Thanks!

Thanks for fixing the post.

By Ehud Lamm at Sat, 2007-02-03 21:48 | login or register to post comments

[Style fixed]

Thanks for pointing those out, Ehud.

By Jim Apple at Sat, 2007-02-03 21:49 | login or register to post comments