Abstract
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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Bauer, A., & Stone, C. A. (2007). RZ: A tool for bringing constructive and computable mathematics closer to programming practice. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4497 LNCS, pp. 28–42). https://doi.org/10.1007/978-3-540-73001-9_4
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
