Floating-point arithmetic in the Coq system
From MaRDI portal
Publication:714617
DOI10.1016/j.ic.2011.09.005zbMath1257.68131OpenAlexW2079624081MaRDI QIDQ714617
Publication date: 11 October 2012
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2011.09.005
Related Items
An approximation framework for solvers and decision procedures, Proving tight bounds on univariate expressions with elementary functions in Coq, Finding normal binary floating-point factors efficiently, Deciding floating-point logic with abstract conflict driven clause learning, Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions, Formal Proofs for Nonlinear Optimization
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- A proof of the Kepler conjecture
- Proving Bounds on Real-Valued Functions with Computations
- MPFR
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- Table-driven implementation of the logarithm function in IEEE floating-point arithmetic
- Fast evaluation of elementary mathematical functions with correctly rounded last bit
- Theorem Proving in Higher Order Logics
