Primitive Floats in Coq

DOI10.4230/LIPIcs.ITP.2019.7OpenAlexW2981852708MaRDI QIDQ5875413

Pierre Roux, Guillaume Bertholon, Érik Martin-Dorel

Publication date: 3 February 2023

Full work available at URL: https://hal.archives-ouvertes.fr/hal-02449191

zbMATH Keywords

floating-point arithmeticCholesky decompositionCoq formal proofsreflexive tactics

Mathematics Subject Classification ID

Related Items (1)

Enabling floating-point arithmetic in the Coq proof assistant

Uses Software

• Coq
• mctoolbox
• Flocq
• CR-LIBM
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Fast machine words in Isabelle/HOL
• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Computing predecessor and successor in rounding to nearest
• Verification of positive definiteness
• A floating-point technique for extending the available precision
• Verification methods: Rigorous results using floating-point arithmetic
• Refinements for Free!
• A compiled implementation of strong reduction
• A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
• Handbook of Floating-Point Arithmetic
• On relative errors of floating-point operations: Optimal bounds and applications
• Accurate Floating-Point Summation Part I: Faithful Rounding
• Formal Proofs for Nonlinear Optimization
• On the Computation of Correctly Rounded Sums
• A FORMAL PROOF OF THE KEPLER CONJECTURE
• Quasi double-precision in floating point addition
• Extending Coq with Imperative Features and Its Application to SAT Verification

This page was built for publication: Primitive Floats in Coq