Flocq

gitlab.inria.frsite

Formalization of floating-point numbers and computations.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   Floating-Point Numbers and Formal Proof github.com

   tool category #coq link ↗

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

   
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. ▲
   Gappa gitlab.inria.fr

   site category #coq link ↗

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

   
5. ▲
   Coquelicot gitlab.inria.fr

   site category #coq link ↗

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

   
6. ▲
   Coq coq.inria.fr

   site category #ocaml link ↗
   

Coq › Projects > Libraries: “Formalization of floating-point numbers and computations.”