Floating-Point Numbers and Formal Proof

github.comtool

Introductory course on Coq real numbers and floating-point numbers from the Flocq library.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   Flocq gitlab.inria.fr

   site category #coq link ↗

   Formalization of floating-point numbers and computations.

   
2. ▲
   Computer Arithmetic and Formal Proofs sciencedirect.com

   site category #coq link ↗

   Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.

3. ▲
   VCFloat github.com

   tool category #coq link ↗

   Framework for verifying C programs with floating-point computations.

   
4. ▲
   Bignums github.com

   tool category #coq link ↗

   Library of arbitrarily large numbers.

   
5. ▲
   Coquelicot gitlab.inria.fr

   site category #coq link ↗

   Formalization of classical real analysis compatible with the standard library and focusing on usability.

   
6. ▲
   Gappa gitlab.inria.fr

   site category #coq link ↗

   Tactic for discharging goals about floating-point arithmetic and round-off errors.

   

Coq › Resources > Course Material: “Introductory course on Coq real numbers and floating-point numbers from the Flocq library.”