Document Open Access Logo

A Certificate-Based Approach to Formally Verified Approximations

Authors Florent Bréhard, Assia Mahboubi, Damien Pous

Thumbnail PDF


  • Filesize: 0.54 MB
  • 19 pages

Document Identifiers

Author Details

Florent Bréhard
  • Plume and AriC teams, LIP, ENS de Lyon, Université de Lyon, Lyon, France
  • MAC team, LAAS-CNRS, Université de Toulouse, CNRS, Toulouse, France
Assia Mahboubi
  • Gallinette team, LS2N, INRIA, Université de Nantes, Nantes, France
Damien Pous
  • Plume team, LIP, CNRS, ENS de Lyon, Université de Lyon, Lyon, France

Cite AsGet BibTex

Florent Bréhard, Assia Mahboubi, and Damien Pous. A Certificate-Based Approach to Formally Verified Approximations. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 8:1-8:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • approximation theory
  • Chebyshev polynomials
  • Banach fixed-point theorem
  • interval arithmetic
  • Coq


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail