Sciweavers

Share
FLOPS
2008
Springer

Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base

10 years 1 months ago
Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
In this paper we describe some certified algorithms for exact real arithmetic based on co-recursion. Our work is based on previous experiences using redundant digits of base 2 but generalizes them using arbitrary integer bases. The goal is to take benefit of fast native integer computation. We extend a technique to compute converging series. We use this technique to compute the product and the inverse. We describe how we implement and certify our algorithms in the proof system Coq and evaluate the efficiency of the library inside the prover.
Nicolas Julien
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FLOPS
Authors Nicolas Julien
Comments (0)
books