Pages that link to "Item:Q331615"
From MaRDI portal
The following pages link to Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615):
Displaying 7 items.
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- A verified ODE solver and the Lorenz attractor (Q1663218) (← links)
- Formally verified approximations of definite integrals (Q1722649) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Primitive Floats in Coq (Q5875413) (← links)
- A certificate-based approach to formally verified approximations (Q5875414) (← links)
- Enabling floating-point arithmetic in the Coq proof assistant (Q6053846) (← links)
