Gappa

gitlab.inria.frsite

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

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. ▲
   GMP gmplib.org

   site category #cpp link ↗

   A C library for arbitrary precision arithmetic, operating on signed integers, rational numbers, and floating-point numbers. [LGPL3 & GPL2]

3. ▲
   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.

   
4. ▲
   VCFloat github.com

   tool category #coq link ↗

   Framework for verifying C programs with floating-point computations.

   
5. ▲
   Gagallium gallium.inria.fr

   site category #ocaml link ↗
6. ▲
   fpdecimal github.com

   tool category #go link ↗

   Fast and precise serialization and arithmetic for small fixed-point decimals

   

Coq › Projects > Plugins: “Tactic for discharging goals about floating-point arithmetic and round-off errors.”