Computer Science – Mathematical Software
Scientific paper
2001-07-19
Computer Science
Mathematical Software
21 pages, web links
Scientific paper
Most existing implementations of multiple precision arithmetic demand that the user sets the precision {\em a priori}. 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 four tools. The tool that contains 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 results 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.
Boldo Sylvie
Daumas Marc
Moreau-Finot Claire
Théry Laurent
No associations
LandOfFree
Computer validated proofs of a toolset for adaptable arithmetic does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Computer validated proofs of a toolset for adaptable arithmetic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Computer validated proofs of a toolset for adaptable arithmetic will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-657537