A certificate-based approach to formally verified approximations - Archive ouverte HAL Access content directly
Conference Papers Year : 2019

A certificate-based approach to formally verified approximations

(1, 2, 3, 4) , (5, 6) , (3, 4)
1
2
3
4
5
6

Abstract

We present a library to verify rigorous approximations of univariate functions on real numbers, with the Coq proof assistant. Based on interval arithmetic, this library also implements a technique of validation a posteriori based on the Banach fixed-point theorem. We illustrate this technique on the case of operations of division and square root. This library features a collection of abstract structures that organise the specfication of rigorous approximations, and modularise the related proofs. Finally, we provide an implementation of verified Chebyshev approximations, and we discuss a few examples of computations.
Fichier principal
Vignette du fichier
chebapprox.pdf (507.62 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02088529 , version 1 (03-04-2019)
hal-02088529 , version 2 (01-07-2019)

Identifiers

Cite

Florent Bréhard, Assia Mahboubi, Damien Pous. A certificate-based approach to formally verified approximations. ITP 2019 - Tenth International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.1-19, ⟨10.4230/LIPIcs.ITP.2019.8⟩. ⟨hal-02088529v2⟩
246 View
12 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More