RZ: A Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice

13 years 10 months ago

Download www.cs.hmc.edu

Realizability theory is not just a fundamental tool in logic and computability. It also has direct application to the design and implementation of programs, since it can produce code 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 speciﬁcations 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.

Andrej Bauer, Christopher A. Stone

Real-time Traffic