A certificate-based approach to formally verified approximations

This page is a web appendix to the following paper.

Authors

Florent Bréhard, Assia Mahboubi, Damien Pous

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.

Coq library

Description of the modules

Modules dependencies