A certificate-based approach to formally verified approximations

Florent Bréhard; Assia Mahboubi; Damien Pous

doi:10.4230/LIPIcs.ITP.2019.8

A certificate-based approach to formally verified approximations

Florent Bréhard, Assia Mahboubi, Damien Pous

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	10th International Conference on Interactive Theorem Proving, ITP 2019
Editors	John Harrison, John O'Leary, Andrew Tolmach
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)	9783959771221
DOIs	https://doi.org/10.4230/LIPIcs.ITP.2019.8
Publication status	Published - 1 Sept 2019
Externally published	Yes
Event	10th International Conference on Interactive Theorem Proving, ITP 2019 - Portland, United States Duration: 9 Sept 2019 → 12 Sept 2019

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	141
ISSN (Print)	1868-8969

Conference

Conference	10th International Conference on Interactive Theorem Proving, ITP 2019
Country/Territory	United States
City	Portland
Period	9/09/19 → 12/09/19

Funding

Funding This work has been funded by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157), and was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program “Investissements d’Avenir” (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR). This work was supported in part by the project FastRelax ANR-14-CE25-0018-01.

Funders	Funder number
European Union’s Horizon 2020 programme
LABEX MILYON	ANR-10-LABX-0070
Horizon 2020 Framework Programme	678157
European Research Council
Agence Nationale de la Recherche	ANR-14-CE25-0018-01
Université de Lyon	ANR-11-IDEX-0007

Keywords

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

Access to Document

10.4230/LIPIcs.ITP.2019.8

Persistent URL (handle)

Persistent link

Cite this

Bréhard, F., Mahboubi, A., & Pous, D. (2019). A certificate-based approach to formally verified approximations. In J. Harrison, J. O'Leary, & A. Tolmach (Eds.), 10th International Conference on Interactive Theorem Proving, ITP 2019 Article 8 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 141). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.ITP.2019.8

Bréhard, Florent ; Mahboubi, Assia ; Pous, Damien. / A certificate-based approach to formally verified approximations. 10th International Conference on Interactive Theorem Proving, ITP 2019. editor / John Harrison ; John O'Leary ; Andrew Tolmach. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2019. (Leibniz International Proceedings in Informatics, LIPIcs).

@inproceedings{3e7654f320c54d6ab122ce0c623fc195,

title = "A certificate-based approach to formally verified approximations",

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.",

keywords = "Approximation theory, Banach fixed-point theorem, Chebyshev polynomials, Coq, Interval arithmetic",

author = "Florent Br{\'e}hard and Assia Mahboubi and Damien Pous",

year = "2019",

month = sep,

day = "1",

doi = "10.4230/LIPIcs.ITP.2019.8",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

editor = "John Harrison and John O'Leary and Andrew Tolmach",

booktitle = "10th International Conference on Interactive Theorem Proving, ITP 2019",

note = "10th International Conference on Interactive Theorem Proving, ITP 2019 ; Conference date: 09-09-2019 Through 12-09-2019",

}

Bréhard, F, Mahboubi, A & Pous, D 2019, A certificate-based approach to formally verified approximations. in J Harrison, J O'Leary & A Tolmach (eds), 10th International Conference on Interactive Theorem Proving, ITP 2019., 8, Leibniz International Proceedings in Informatics, LIPIcs, vol. 141, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 10th International Conference on Interactive Theorem Proving, ITP 2019, Portland, United States, 9/09/19. https://doi.org/10.4230/LIPIcs.ITP.2019.8

A certificate-based approach to formally verified approximations. / Bréhard, Florent; Mahboubi, Assia; Pous, Damien.
10th International Conference on Interactive Theorem Proving, ITP 2019. ed. / John Harrison; John O'Leary; Andrew Tolmach. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2019. 8 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 141).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - A certificate-based approach to formally verified approximations

AU - Bréhard, Florent

AU - Mahboubi, Assia

AU - Pous, Damien

PY - 2019/9/1

Y1 - 2019/9/1

N2 - 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.

AB - 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.

KW - Approximation theory

KW - Banach fixed-point theorem

KW - Chebyshev polynomials

KW - Coq

KW - Interval arithmetic

UR - http://www.scopus.com/inward/record.url?scp=85074591554&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85074591554&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.ITP.2019.8

DO - 10.4230/LIPIcs.ITP.2019.8

M3 - Conference contribution

AN - SCOPUS:85074591554

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 10th International Conference on Interactive Theorem Proving, ITP 2019

A2 - Harrison, John

A2 - O'Leary, John

A2 - Tolmach, Andrew

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 10th International Conference on Interactive Theorem Proving, ITP 2019

Y2 - 9 September 2019 through 12 September 2019

ER -

Bréhard F, Mahboubi A, Pous D. A certificate-based approach to formally verified approximations. In Harrison J, O'Leary J, Tolmach A, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2019. 8. (Leibniz International Proceedings in Informatics, LIPIcs). doi: 10.4230/LIPIcs.ITP.2019.8

A certificate-based approach to formally verified approximations

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this