The members of the CoqApprox working group include Nicolas Brisebarre, Mioara Joldes, Erik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, and Laurent Théry.

We develop a formalization of rigorous polynomial approximation using Taylor models inside the Coq proof assistant, with a special focus on genericity and efficiency for the computations.

The CoqApprox library is now part of CoqInterval

CoqApprox is now maintained and distributed within the CoqInterval library, version 2.0.0 and later.

Download the library

You can download the code of our CoqApprox library: coqapprox-2.0.0.tar.gz (80 KiB).

Browse the theories

You can also browse the CoqApprox theories online (version 2.0.0).


The CoqApprox library is based on the following tools and libraries:


This work has been presented at the 4th NASA Formal Methods symposium NFM 2012 (slides), and a report appears in Volume 7226/2012 of the Lecture Notes in Computer Science (Springer): Rigorous Polynomial Approximation using Taylor Models in Coq, pages 85-99 (DOI). Author version available in open archive.

The formal proofs having been completed, version 2.0.0 of the library has been presented at the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing SYNASC 2013 (slides), and a report appears in the post-proceedings (IEEE CPS, 2013): Certified, Efficient and Sharp Univariate Taylor Models in COQ, pages 193-200 (DOI). Author version available in open archive.

Return to the TaMaDi web page  |  Go to the CoqInterval web page.

Last modified: Tuesday 2015-10-13, 20:19:51 +0200 Valid XHTML 1.0 Strict!   Valid CSS!