Certified, Efficient and Sharp Univariate Taylor Models in COQ
| Autor: | Erik Martin-Dorel, Laurence Rideau, Ioana Pasca, Micaela Mayero, Laurent Théry |
|---|---|
| Přispěvatelé: | Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Logic, Computation and Reasoning [Villetaneuse] (LCR), Laboratoire d'Informatique de Paris-Nord (LIPN), Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS)-Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS), Institut Universitaire Technologique de Nîmes (IUT [Nîmes]), IUT de Nîmes, Martin-Dorel, Érik, Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Cité (USPC)-Institut Galilée-Université Paris 13 (UP13)-Centre National de la Recherche Scientifique (CNRS) |
| Rok vydání: | 2013 |
| Předmět: |
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Correctness univariate Taylor models COQ proof assistant 0102 computer and information sciences 02 engineering and technology Mathematical proof 01 natural sciences Set (abstract data type) rigorous polynomial approximation Square root 0202 electrical engineering electronic engineering information engineering formal verification Formal verification Mathematics [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC] [INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC] Proof assistant Univariate [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering computer.file_format [INFO.INFO-NA]Computer Science [cs]/Numerical Analysis [cs.NA] Algebra 010201 computation theory & mathematics [INFO.INFO-NA] Computer Science [cs]/Numerical Analysis [cs.NA] TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Mathematical Software Executable computer |
| Zdroj: | SYNASC SYNASC 2013-15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing SYNASC 2013-15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2013, Timisoara, Romania |
| Popis: | We present a library for univariate Taylor models that has been developed with the COQ proof assistant. Each algorithm of this library is executable and has been formally proved correct. Using this library, one can then effectively compute rigorous and sharp approximations of univariate functions composed of usual functions such as reciprocal, square root, exponential, or sine among others. In this paper, we present the key parts of the formalisation as well as of the proofs of correctness, and we evaluate the quality of our certified library on a set of examples. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|