Primitive Floats in Coq
From MaRDI portal
Publication:5875413
Cites work
- scientific article; zbMATH DE number 3473265 (Why is no real title available?)
- scientific article; zbMATH DE number 846277 (Why is no real title available?)
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
- A compiled implementation of strong reduction
- A floating-point technique for extending the available precision
- A formal proof of the Kepler conjecture
- Accurate Floating-Point Summation Part I: Faithful Rounding
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Computing predecessor and successor in rounding to nearest
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Fast machine words in Isabelle/HOL
- Formal Proofs for Nonlinear Optimization
- Formal proof - the four color theorem
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
- Handbook of Floating-Point Arithmetic
- On relative errors of floating-point operations: optimal bounds and applications
- On the Computation of Correctly Rounded Sums
- Proof-assistants using dependent type systems
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Quasi double-precision in floating point addition
- Refinements for free!
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Verification methods: rigorous results using floating-point arithmetic
- Verification of positive definiteness
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)
