A certificate-based approach to formally verified approximations

Florent Bréhard, Assia Mahboubi, Damien Pous

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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.

Original languageEnglish
Title of host publication10th International Conference on Interactive Theorem Proving, ITP 2019
EditorsJohn Harrison, John O'Leary, Andrew Tolmach
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959771221
DOIs
Publication statusPublished - 1 Sep 2019
Externally publishedYes
Event10th International Conference on Interactive Theorem Proving, ITP 2019 - Portland, United States
Duration: 9 Sep 201912 Sep 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume141
ISSN (Print)1868-8969

Conference

Conference10th International Conference on Interactive Theorem Proving, ITP 2019
CountryUnited States
CityPortland
Period9/09/1912/09/19

Keywords

  • Approximation theory
  • Banach fixed-point theorem
  • Chebyshev polynomials
  • Coq
  • Interval arithmetic

Fingerprint

Dive into the research topics of 'A certificate-based approach to formally verified approximations'. Together they form a unique fingerprint.

Cite this