Proving Bounds on Real-Valued Functions with Computations
From MaRDI portal
Recommendations
Cites work
- A Computational Approach to Pocklington Certificates in Type Theory
- A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
- Formal Global Optimisation with Taylor Models
- scientific article; zbMATH DE number 1595639 (Why is no real title available?)
- scientific article; zbMATH DE number 1696760 (Why is no real title available?)
- scientific article; zbMATH DE number 3649911 (Why is no real title available?)
- scientific article; zbMATH DE number 1863384 (Why is no real title available?)
- Implementing the cylindrical algebraic decomposition within the Coq system
- Theorem Proving in Higher Order Logics
- Verifying Nonlinear Real Formulas Via Sums of Squares
Cited in
(24)- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- Coquelicot: a user-friendly library of real analysis for Coq
- Axiomatic reals and certified efficient exact real computation
- Formalization of Bernstein polynomials and applications to global optimization
- Formally verified approximations of definite integrals
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Affine arithmetic and applications to real-number proving
- Certification of bounds on expressions involving rounded operators
- scientific article; zbMATH DE number 5862941 (Why is no real title available?)
- Hardware-Dependent Proofs of Numerical Programs
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Combining Coq and Gappa for Certifying Floating-Point Programs
- Computable analysis and notions of continuity in \textsc{Coq}
- Theorem Proving in Higher Order Logics
- Multi-prover verification of floating-point programs
- A certificate-based approach to formally verified approximations
- Formally-verified round-off error analysis of Runge-Kutta methods
- Semantics, specification logic, and Hoare logic of exact real computation
- Computable analysis for verified exact real computation
- Robust Mean estimation by all means (short paper)
- Extracting efficient exact real number computation from proofs in constructive type theory
- Floating-point arithmetic in the Coq system
- Formalizing concentration inequalities in Rocq: infrastructure and automation
- Computing the range of values of real functions with accuracy higher than second order
This page was built for publication: Proving Bounds on Real-Valued Functions with Computations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3541683)
