Arithmétique des Ordinateurs Certifiée
(Certified Arithmetic)

Cooperative Research Action


Building certified numeric softwares only makes sense if the elementary arithmetic that is used is also certified. Recent examples show that there is no obvious way of completing this task and still more research has to be done in that area. The goal of the action is to bring together several research teams whose interests include formal proofs, designing new algorithm, implementing efficient arithmetic libraries.

AOC members

Lemme Project

Polka Project

Arénaire Project



Feb. 00: First meeting (french)
Jun. 00: Second meeting (french)
Nov. 00: Workshop


People: Harrison Kahan, Russinoff

Resources: Open Source for Numerics,Correctness of Iterative Square Root

Laurent Théry