Pages that link to "Item:Q714617"
From MaRDI portal
The following pages link to Floating-point arithmetic in the Coq system (Q714617):
Displaying 21 items.
- Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615) (← links)
- Twin-float arithmetic (Q412221) (← links)
- Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
- Formalization of fixed-point arithmetic in HOL (Q816219) (← links)
- Formal verification of a floating-point expansion renormalization algorithm (Q1687723) (← links)
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check (Q2013318) (← links)
- Formally verified certificate checkers for hardest-to-round computation (Q2352500) (← links)
- Verified compilation of floating-point computations (Q2352505) (← links)
- An approximation framework for solvers and decision procedures (Q2362497) (← links)
- Stupid is as stupid does: taking the square root of the square of a floating-point number (Q2520675) (← links)
- A parameterized floating-point formalizaton in HOL Light (Q2520685) (← links)
- LNS with Co-Transformation Competes with Floating-Point (Q2985681) (← links)
- (Q4011800) (← links)
- Optimizing floating point operations in Scheme (Q4951520) (← links)
- FloatX (Q4960963) (← links)
- Formal Proofs for Nonlinear Optimization (Q5195260) (← links)
- Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions (Q5206960) (← links)
- Floating-Point LLL Revisited (Q5385731) (← links)
- Types for Proofs and Programs (Q5712314) (← links)
- Finding normal binary floating-point factors efficiently (Q6156639) (← links)
- SAT Modulo Differential Equation Simulations (Q6487261) (← links)
