LIPIcs.ITP.2019.8.pdf
- Filesize: 0.54 MB
- 19 pages
Document
A Certificate-Based Approach to Formally Verified Approximations
Authors
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
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)
https://doi.org/10.4230/LIPIcs.ITP.2019.8
https://doi.org/10.4230/LIPIcs.ITP.2019.8
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic
Keywords
- approximation theory
- Chebyshev polynomials
- Banach fixed-point theorem
- interval arithmetic
- Coq
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads