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.
Keywords for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
- Martin-Dorel, Érik; Melquiond, Guillaume: Proving tight bounds on univariate expressions with elementary functions in Coq (2016)
- Roux, Pierre: Formal proofs of rounding error bounds. With application to an automatic positive definiteness check (2016)
- Boldo, Sylvie: Stupid is as stupid does: taking the square root of the square of a floating-point number (2015)
- Boldo, Sylvie; Jourdan, Jacques-Henri; Leroy, Xavier; Melquiond, Guillaume: Verified compilation of floating-point computations (2015)
- Jacobsen, Charles; Solovyev, Alexey; Gopalakrishnan, Ganesh: A parameterized floating-point formalizaton in HOL Light (2015)
- Roux, Pierre; Garoche, Pierre-Loïc: Practical policy iterations. A practical use of policy iterations for static analysis: the quadratic case (2015)
- Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Trusting computations: a mechanized proof from partial differential equations to actual program (2014)
- Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)
- Krebbers, Robbert; Spitters, Bas: Type classes for efficient exact real arithmetic in Coq (2013)
- Collins, Pieter; Niqui, Milad; Revol, Nathalie: A validated real function calculus (2011)
- Krebbers, Robbert; Spitters, Bas: Computer certified efficient exact reals in Coq (2011)