Computer Validated Proofs of a Toolset for Adaptable Arithmetic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2001

Computer Validated Proofs of a Toolset for Adaptable Arithmetic

Marc Daumas
  • Fonction : Auteur
Laurent Théry

Résumé

Most existing implementations of multiple precision arithmetic demand that the user sets the precision a priori. A solution is to use the largest precision necessary to reach target accuracy. Some libraries are said adaptable in the sense that they dynamically change the precision of each intermediate operation individually to deliver the target accuracy according to the actual inputs. We present in this text a new adaptable numeric core inspired both from floating point expansions and from on-line arithmetic. The numeric core is cut down to five tools. The first tool that contains many arithmetic operations is proved to be correct. The proofs have been formally checked by the Coq assistant. Developing the proofs, we have formally proved many result published in the literature and we have extended a few of them. This work may let users (i) develop application specific adaptable libraries based on the toolset and / or (ii) write new formal proofs based on the set of validated facts.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-4095.pdf (490.79 Ko) Télécharger le fichier
RR2001-01.pdf (628.5 Ko) Télécharger le fichier

Dates et versions

inria-00072536 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00072536 , version 1

Citer

Marc Daumas, Claire Moreau-Finot, Laurent Théry. Computer Validated Proofs of a Toolset for Adaptable Arithmetic. [Research Report] RR-4095, LIP RR2001-01, INRIA, LIP. 2001. ⟨inria-00072536⟩
70 Consultations
318 Téléchargements

Partager

Gmail Facebook X LinkedIn More