Sciweavers

ENTCS
2008

Implementing Real Numbers With RZ

13 years 11 months ago
Implementing Real Numbers With RZ
RZ is a tool which translates axiomatizations of mathematical structures to program specifications using the realizability interpretation of logic. This helps programmers correctly implement data structures for computable mathematics. RZ does not prescribe a particular method of implementation, but allows programmers to write efficient code by hand, or to extract trusted code from formal proofs, if they so desire. We used this methodology to axiomatize real numbers and implemented the specification computed by RZ. The axiomatization is the standard domaintheoretic construction of reals as the maximal elements of the interval domain, while the implementation closely follows current state-of-the-art implementations of exact real arithmetic. Our results shows not only that the theory and practice of computable mathematics can coexist, but also that they work together harmoniously.
Andrej Bauer, Iztok Kavkler
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Andrej Bauer, Iztok Kavkler
Comments (0)