A certificate-based approach to formally verified approximations

Florent Bréhard 1, 2, 3, 4 Assia Mahboubi 5, 6 Damien Pous 3, 4
1 LAAS-MAC - Équipe Méthodes et Algorithmes en Commande
LAAS - Laboratoire d'analyse et d'architecture des systèmes [Toulouse]
2 ARIC - Arithmetic and Computing
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
3 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
5 GALLINETTE - Gallinette : vers une nouvelle génération d'assistant à la preuve
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
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.
Complete list of metadatas

Cited literature [39 references]  Display  Hide  Download

https://hal.laas.fr/hal-02088529
Contributor : Damien Pous <>
Submitted on : Monday, July 1, 2019 - 10:32:54 PM
Last modification on : Friday, July 5, 2019 - 3:38:17 PM

File

chebapprox.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02088529, version 2

Citation

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. ⟨hal-02088529v2⟩

Share

Metrics

Record views

114

Files downloads

24