Primitive Floats in Coq
From MaRDI portal
Publication:5875413
DOI10.4230/LIPICS.ITP.2019.7OpenAlexW2981852708MaRDI QIDQ5875413FDOQ5875413
Authors: Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux 
Publication date: 3 February 2023
Full work available at URL: https://hal.archives-ouvertes.fr/hal-02449191
Cites Work
- Title not available (Why is that?)
- Verification methods: rigorous results using floating-point arithmetic
- Title not available (Why is that?)
- Accurate Floating-Point Summation Part I: Faithful Rounding
- Formal proof - the four color theorem
- Computing predecessor and successor in rounding to nearest
- A floating-point technique for extending the available precision
- Refinements for free!
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Handbook of Floating-Point Arithmetic
- Verification of positive definiteness
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
- Proof-assistants using dependent type systems
- Fast machine words in Isabelle/HOL
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- A formal proof of the Kepler conjecture
- A compiled implementation of strong reduction
- On relative errors of floating-point operations: optimal bounds and applications
- Quasi double-precision in floating point addition
- Formal Proofs for Nonlinear Optimization
- Extending Coq with Imperative Features and Its Application to SAT Verification
- On the Computation of Correctly Rounded Sums
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
Cited In (1)
Uses Software
This page was built for publication: Primitive Floats in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875413)
