RZ: A Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice. Realizability theory can produce interfaces for the data structure corresponding to a mathematical theory. Our tool, called RZ, serves as a bridge between constructive mathematics and programming by translating 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.
Keywords for this software
References in zbMATH (referenced in 6 articles , 1 standard article )
Showing results 1 to 6 of 6.
- Berger, Ulrich: Realisability for induction and coinduction with applications to constructive analysis (2010)
- Bauer, Andrej; Kavkler, Iztok: A constructive theory of continuous domains suitable for implementation (2009)
- Bauer, Andrej; Stone, Christopher A.: RZ: a tool for bringing constructive and computable mathematics closer to programming practice (2009)
- Berger, Ulrich: Realisability and adequacy for (co)induction (2009)
- Bauer, Andrej; Kavkler, Iztok: Implementing real numbers with RZ. (2008)
- Bauer, Andrej; Stone, Christopher A.: RZ: A tool for bringing constructive and computable mathematics closer to programming practice (2007)