A certificate-based approach to formally verified approximations

DOI10.4230/LIPIcs.ITP.2019.8OpenAlexW2936040140MaRDI QIDQ5875414

Florent Bréhard, Damien Pous, Assia Mahboubi

Publication date: 3 February 2023

Full work available at URL: https://laas.hal.science/hal-02088529

zbMATH Keywords

Chebyshev polynomialsinterval arithmeticapproximation theoryBanach fixed-point theoremCoq

Mathematics Subject Classification ID

Related Items (3)

A certificate-based approach to formally verified approximations ⋮ A symbolic-numeric validation algorithm for linear ODEs with Newton-Picard method ⋮ Verified interactive computation of definite integrals

Uses Software

• Coq
• C-XSC
• C-XSC 2.0
• MPFI
• INTLAB
• Chebfun
• Arb
• kepler98
• RODES

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proving tight bounds on univariate expressions with elementary functions in Coq
• Formal and efficient primality proofs by use of computer algebra oracles
• Iterative approximation of fixed points
• A Skeptic's approach to combining HOL and Maple
• Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models
• A rigorous ODE solver and Smale's 14th problem
• Autarkic computations in formal proofs
• A verified ODE solver and the Lorenz attractor
• Formally verified approximations of definite integrals
• Motivations for an arbitrary precision interval arithmetic and the MPFI library
• Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach
• Chebyshev interpolation polynomial-based tools for rigorous computing
• Rigorous uniform approximation of D-finite functions using Chebyshev expansions
• Proving Bounds on Real-Valued Functions with Computations
• A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
• Chaotic Braided Solutions via Rigorous Numerics: Chaos in the Swift–Hohenberg Equation
• A Numerical Verification Method for Solutions of Boundary Value Problems with Local Uniqueness by Banach's Fixed-Point Theorem
• Arb: Efficient Arbitrary-Precision Midpoint-Radius Interval Arithmetic
• Validated and Numerically Efficient Chebyshev Spectral Methods for Linear Ordinary Differential Equations
• A Quartic System with Twenty-Six Limit Cycles
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Rigorous Numerics for Nonlinear Differential Equations Using Chebyshev Series
• Theorem Proving in Higher Order Logics
• A certificate-based approach to formally verified approximations

This page was built for publication: A certificate-based approach to formally verified approximations