文章基本信息

标题：A Certificate-Based Approach to Formally Verified Approximations
本地全文：下载
作者：Florent Brhard ; Assia Mahboubi ; Damien Pous 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：141
页码：1-19
DOI：10.4230/LIPIcs.ITP.2019.8
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：approximation theory; Chebyshev polynomials; Banach fixed-point theorem; interval arithmetic; Coq