Enabling floating-point arithmetic in the Coq proof assistant

DOI10.1007/s10817-023-09679-xMaRDI QIDQ6053846

Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux

Publication date: 24 October 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

floating-point arithmeticformal proofproof by computation

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Proving tight bounds on univariate expressions with elementary functions in Coq
• A rigorous ODE solver and Smale's 14th problem
• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
• Verified compilation of floating-point computations
• Verification of positive definiteness
• 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
• On relative errors of floating-point operations: Optimal bounds and applications
• Handbook of Floating-Point Arithmetic
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Primitive Floats in Coq

This page was built for publication: Enabling floating-point arithmetic in the Coq proof assistant