Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Rigorous Polynomial Approximation using Taylor Models in Coq

Abstract : One of the most common and practical ways of representing a real function on machines is by using a polynomial approximation. It is then important to properly handle the error introduced by such an approximation. The purpose of this work is to offer certified error bounds for a specific kind of rigorous polynomial approximation called Taylor model. We carry out this work in the Coq proof assistant, with a special focus on genericity and efficiency for our implementation. We give an abstract interface for rigorous polynomial approximations, parameterized by the type of coefficients and the implementation of polynomials, and we instantiate this interface to the case of Taylor models with interval coefficients, while providing all the machinery for computing them. We compare the performances of our implementation in Coq with those of the Sollya tool, which contains an implementation of Taylor models written in C. This is a milestone in our long-term goal of providing fully formally certified and efficient Taylor models.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal-ens-lyon.archives-ouvertes.fr/ensl-00653460
Contributor : Jean-Michel Muller <>
Submitted on : Monday, December 19, 2011 - 3:30:58 PM
Last modification on : Friday, September 10, 2021 - 2:34:02 PM
Long-term archiving on: : Friday, November 16, 2012 - 4:00:42 PM

File

coq-approx.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : ensl-00653460, version 1

Citation

Nicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, et al.. Rigorous Polynomial Approximation using Taylor Models in Coq. 2011. ⟨ensl-00653460v1⟩

Share

Metrics

Record views

175

Files downloads

143