Bibliography
============

Description of Gappa
--------------------

Marc Daumas and Guillaume Melquiond.
`Certification of bounds on expressions involving rounded operators
<http://dx.doi.org/10.1145/1644001.1644003>`_.
*ACM Transactions on Mathematical Software*. 37(1):1-20. 2010.

Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin,
Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie
Revol, Damien Stehlé, and Serge Torres.
`Handbook of Floating-Point Arithmetic
<http://dx.doi.org/10.1007/978-0-8176-4705-6_15>`_.
Birkhäuser, 2010.

Applications of Gappa
---------------------

Guillaume Melquiond and Sylvain Pion.
`Formally certified floating-point filters for homogeneous geometric predicates
<http://dx.doi.org/10.1051/ita:2007005>`_.
*Theoretical Informatics and Applications*. 41(1):57­-70. 2007.

Arnaud Tisserand.
`High-performance hardware operators for polynomial evaluation
<http://dx.doi.org/10.1504/IJHPSA.2007.013288>`_.
*International Journal of High Performance Systems Architecture*. 1(1):14-23. 2007.

Christoph Lauter and Florent de Dinechin.
`Optimizing polynomials for floating-point implementation
<http://hal.archives-ouvertes.fr/ensl-00260563/>`_.
*Proceedings of the 8th Conference on Real Numbers and Computers*. 7-16.
Santiago de Compostella, Spain. 2008.

Sylvie Boldo, Marc Daumas, and Pascal Giorgi.
`Formal proof for delayed finite field arithmetic using floating point operators
<http://hal.archives-ouvertes.fr/hal-00135090/>`_.
*Proceedings of the 8th Conference on Real Numbers and Computers*. 113-122.
Santiago de Compostella, Spain. 2008.

Sylvie Boldo, Jean-Christophe Filliâtre, and Guillaume Melquiond.
`Combining Coq and Gappa for certifying floating-point programs
<http://dx.doi.org/10.1007/978-3-642-02614-0_10>`_.
*Proceedings of the 16th Calculemus Symposium*. 59-74. Grand Bend, ON, Canada. 2009.

Claude-Pierre Jeannerod and Guillaume Revy.
`Optimizing correctly-rounded reciprocal square roots for embedded VLIW cores
<http://dx.doi.org/10.1109/ACSSC.2009.5469948>`_.
*Proceedings of the 43rd Asilomar Conference on Signals, Systems and Computers*.
731-735. Pacific Grove, CA, USA. 2009.

Claude-Pierre Jeannerod, Hervé Knochel, Christophe Monat, Guillaume Revy,
and Gilles Villard.
`A new binary floating-point division algorithm and its software implementation
on the ST231 processor
<http://dx.doi.org/10.1109/ARITH.2009.19>`_.
*Proceedings of the 19th Symposium on Computer Arithmetic*. 95-103.
Portland, OR, USA. 2009.

Michael D. Linderman, Matthew Ho, David L. Dill, Teresa H. Meng, Garry
P. Nolan. `Towards program optimization through automated analysis of
numerical precision <http://dx.doi.org/10.1145/1772954.1772987>`_.
*Proceedings of the 8th International Symposium on Code Generation and
Optimization*. 230-237. Toronto, ON, Canada. 2010.

Vincent Lefèvre, Philippe Théveny, Florent de Dinechin, Claude-Pierre
Jeannerod, Christophe Mouilleron, David Pfannholzer, and Nathalie Revol.
`LEMA: towards a language for reliable arithmetic
<http://dx.doi.org/10.1145/1838599.1838622>`_.
*ACM SIGSAM Bulletin*. 44(1/2):41-52. 2010.

Sylvie Boldo and Thi Minh Tuyen Nguyen.
`Hardware-independent proofs of numerical programs
<http://shemesh.larc.nasa.gov/NFM2010/papers/nfm2010_14_23.pdf>`_.
*Proceedings of the 2nd NASA Formal Methods Symposium*. 14-23.
Washington DC, USA. 2010.

Ali Ayad and Claude Marché.
`Multi-prover verification of floating-point programs
<http://dx.doi.org/10.1007/978-3-642-14203-1_11>`_.
*Proceedings of the 5th International Joint Conference on Automated Reasoning*.
127-141. Edinburgh, Scotland. 2010.

Claude-Pierre Jeannerod, Hervé Knochel, Christophe Monat, and Guillaume Revy.
`Computing floating-point square roots via bivariate polynomial evaluation
<http://dx.doi.org/10.1109/TC.2010.152>`_.
*IEEE Transactions on Computers*. 60(2):214-227. 2011.

Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond.
`Certifying the floating-point implementation of an elementary function
using Gappa <http://dx.doi.org/10.1109/TC.2010.128>`_.
*IEEE Transactions on Computers*. 60(2):242-253. 2011.

Christophe Mouilleron and Guillaume Revy.
`Automatic generation of fast and certified code for polynomial evaluation
<http://dx.doi.org/10.1109/ARITH.2011.39>`_.
*Proceedings of the 20th Symposium on Computer Arithmetic*. 233-242.
Tübingen, Germany. 2011.

Claude-Pierre Jeannerod and Jingyan Jourdan-Lu.
`Simultaneous floating-point sine and cosine for VLIW integer processors
<http://dx.doi.org/10.1109/ASAP.2012.12>`_.
*Proceedings of the 23rd International Conference on Application-Specific
Systems, Architectures and Processors*. 69-76. Delft, The Netherlands. 2012.

Olga Kupriianova and Christoph Lauter.
`Metalibm: A Mathematical Functions Code Generator
<http://dx.doi.org/10.1007/978-3-662-44199-2_106>`_.
*Proceedings of the 4th International Congress on Mathematical Software*.
713-717. Seoul, Korea. 2014.