ExpFloat

Exponential in binary 64

Algorithm FastTwoSum :

• Algorithm FastTwoSum
• Bounds on the error of FastTwoSum

Algorithm ExactMul :

• Algorithm ExactMult
• Lemma 0

Algorithm FastSum :

• Algorithm FastSum
• Lemma 1

Algorithm P1 :

• Algorithm P1
• Absolute error of Sollya polynomial
• Relative error of Sollya polynomial
• Bound of ph of algorithm P1
• Bound of pl of algorithm P1
• Absolute error of algorithm P1 (first part Lemma 2)
• Relative error of algorithm P1
• Refined relative error of algorithm P1 (second part Lemma 2)

Algorithm Log1 :

• Definition of the INVERSE table
• Lemma 3
• Definition of the LOGINV table
• Definition of Log1
• Lemma 4

Algorithm Mul1 :

• Definition of Mul1
• Lemma 5

Algorithm Q1 :

• Definition of the polynomial Q
• Absolute error of the polynomial Q
• Algorithm Q1
• Lemma 6

Algorithm Exp1 :

• table T1
• relative error for T1
• table T2
• relative error for T2
• algorithm Exp1
• Lemma 7

Algorithm Phase1 :

• algorithm Phase 1
• Theorem 1

Meta

• Author(s):
  • Laurent Théry
  • Laurence Rideau
• License: MIT License
• Compatible Coq versions: 8.18 or later
• Additional dependencies:
  • MathComp ssreflect 1.17 or later
  • Coquelicot 3.4.0 or later
  • MathComp algebra 1.17 or later
  • Flocq 4.1.3 or later
  • Interval 4.8.1 or later
• Coq namespace: floatexp
• Related publication(s): none

Building and installation instructions

To build and install manually, do:

git clone https://github.com/thery/expfloat.git
cd expfloat
make   # or make -j <number-of-cores-on-your-machine> 
make install