Abstract:
In this talk we will present a certified library in exact real arithmetic based on co-induction. Our work is inspired by previous experiences using signed digits of radix 2 but generalizes this operations using an arbitrary integer radix. The aim of this formalization is to use fast operations of processor integer arithmetic.
A longer abstract can be found (in french) there.
Résumé:
Nous décrivons dans cet présenation des algorithmes certifiés pour l'arithmétique réelle exacte basée sur la co-récursion. Nos travaux s'inspirent d'expériences précédentes utilisant des chiffres signés en base 2 mais généralisent ces opérations à l'utilisation de bases entières arbitraires. L'objectif est d'utiliser les opérations rapides de l'arithmétique entière des micro-processeurs.
Un résumé plus long peut se trouver ici.