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

https://hal.laas.fr/hal-02088529
Contributor : Florent Bréhard <>
Submitted on : Wednesday, April 3, 2019 - 12:19:20 AM
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 1

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-02088529v1⟩

Share

Metrics

Record views

159

Files downloads

95