Computer Arithmetic and Formal Proofs

sciencedirect.comsite

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

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

   site category #coq link ↗

   Formalization of floating-point numbers and computations.

   
3. ▲
   VCFloat github.com

   tool category #coq link ↗

   Framework for verifying C programs with floating-point computations.

   
4. ▲
   Proofs and Reliable Programming using Coq team.inria.fr

   site category #coq link ↗

   Introduction to developing and verifying programs with Coq.

5. ▲
   Gappa gitlab.inria.fr

   site category #coq link ↗

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

   
6. ▲
   FCF github.com

   tool category #coq link ↗

   Framework for proofs of cryptography.

   

Coq › Resources > Books: “Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.”