F
flocq
Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.
Project ID: 4601
-
Pierre Roux authored
From: Claude-Pierre Jeannerod, Siegfried M. Rump: On relative errors of floating-point operations: Optimal bounds and applications, Math. Comput., 87(310):803-819, 2018. The paper also contain a specific result for division in radix2 (only the generic radix result is proved here).
7ec13200
| Name |
Last commit
|
Last update |
|---|---|---|
| examples | ||
| src | ||
| .gitignore | ||
| .mailmap | ||
| AUTHORS | ||
| COPYING | ||
| INSTALL.md | ||
| NEWS.md | ||
| README.md | ||
| Remakefile.in | ||
| _CoqProject | ||
| autogen.sh | ||
| configure.in | ||
| remake.cpp |