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.

• Type: Conference
• Year: 2008
• Where: FLOPS
• Authors: Nicolas Julien
• Keywords: Arbitrary Integer Bases, Automated Reasoning, Certified Algorithms, Fast Native Integer, FLOPS 2008