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

Descriptions of Gappa
---------------------

Marc Daumas and Guillaume Melquiond.
`Certification of bounds on expressions involving rounded operators
<https://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
<https://dx.doi.org/10.1007/978-0-8176-4705-6_15>`__.
Birkhäuser, 2010.

Sylvie Boldo and Guillaume Melquiond.
Computer Arithmetic and Formal Proofs:
Verifying Floating-point Algorithms with the Coq System.
ISTE Press, 2017.

Jean-Michel Muller, Nicolas Brunie, Florent de Dinechin, Claude-Pierre Jeannerod, Mioara Joldes, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, and Serge Torres,
`Handbook of Floating-Point Arithmetic
<https://dx.doi.org/10.1007/978-3-319-76526-6>`__, 2nd edition.
Birkhäuser, 2018.

Sylvie Boldo and Guillaume Melquiond.
`Some formal tools for computer arithmetic: Flocq and Gappa
<https://hal.science/hal-03233227>`__.
*28th IEEE International Symposium on Computer Arithmetic*.
2021.

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

Guillaume Melquiond and Sylvain Pion.
`Formally certified floating-point filters for homogeneous geometric predicates
<https://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
<https://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
<https://hal.science/ensl-00260563/>`__.
*8th Conference on Real Numbers and Computers*, pp 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
<https://hal.science/hal-00135090/>`__.
*8th Conference on Real Numbers and Computers*, pp 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
<https://dx.doi.org/10.1007/978-3-642-02614-0_10>`__.
*16th Calculemus Symposium*, pp 59-74.
Grand Bend, ON, Canada, 2009.

Claude-Pierre Jeannerod and Guillaume Revy.
`Optimizing correctly-rounded reciprocal square roots for embedded VLIW cores
<https://dx.doi.org/10.1109/ACSSC.2009.5469948>`__.
*43rd Asilomar Conference on Signals, Systems and Computers*, pp 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
<https://dx.doi.org/10.1109/ARITH.2009.19>`__.
*19th IEEE Symposium on Computer Arithmetic*, pp 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
<https://dx.doi.org/10.1145/1772954.1772987>`__.
*8th International Symposium on Code Generation and Optimization*, pp 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
<https://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
<https://hal.science/inria-00534410/>`__.
*2nd NASA Formal Methods Symposium*, pp 14-23.
Washington DC, USA, 2010.

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

Claude-Pierre Jeannerod, Hervé Knochel, Christophe Monat, and Guillaume Revy.
`Computing floating-point square roots via bivariate polynomial evaluation
<https://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 <https://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
<https://dx.doi.org/10.1109/ARITH.2011.39>`__.
*20th Symposium on Computer Arithmetic*, pp 233-242.
Tübingen, Germany, 2011.

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

Olga Kupriianova and Christoph Lauter.
`Metalibm: A mathematical functions code generator
<https://dx.doi.org/10.1007/978-3-662-44199-2_106>`__.
*4th International Congress on Mathematical Software*, pp 713-717.
Seoul, Korea, 2014.

Sylvie Boldo.
`Formal verification of programs computing the floating-point average
<https://doi.org/10.1007/978-3-319-25423-4_2>`__.
17th International Conference on Formal Engineering Methods, pp 17-32.
Paris, France, 2015.

Sylvie Boldo, Florian Faissole, and Alexandre Chapoutot.
`Round-off error analysis of explicit one-step numerical integration methods
<https://doi.org/10.1109/ARITH.2017.22>`__.
*24th IEEE Symposium on Computer Arithmetic*, pp 82-89.
London, UK, 2017.

Guillaume Melquiond and Raphaël Rieu-Helft.
`Formal verification of a state-of-the-art integer square root.
<https://dx.doi.org/10.1109/ARITH.2019.00041>`__.
*26th IEEE Symposium on Computer Arithmetic*, pp 183-186.
Kyoto, Japan, 2019.

David Monniaux and Alice Pain.
`Formally verified 32- and 64-bit integer division using double-precision floating-point arithmetic
<https://doi.org/10.1109/ARITH54963.2022.00032>`__.
*29th IEEE Symposium on Computer Arithmetic*, pp 128-132.
2022.

Paul Geneau de Lamarlière, Guillaume Melquiond, and Florian Faissole.
`Slimmer formal proofs for mathematical libraries
<https://dx.doi.org/10.1109/ARITH58626.2023.00026>`__.
*30th IEEE International Symposium on Computer Arithmetic*, pp 32-35.
Portland, OR, USA, 2023.

Simon Tatham.
`Formally verifying a floating-point division routine with Gappa
<https://developer.arm.com/community/arm-community-blogs/b/embedded-and-microcontrollers-blog/posts/formally-verifying-a-floating-point-division-routine-with-gappa-p1>`__.
ARM, 2025.

Tom Hubrecht and Guillaume Melquiond.
Verifying code that uses error-free transformations.
*33rd IEEE International Symposium on Computer Arithmetic*.
Fulda, Germany, 2026.

Paul Zimmermann.
The GNU libc atanh is correctly rounded.
*33rd IEEE International Symposium on Computer Arithmetic*.
Fulda, Germany, 2026.

Nicolas Brisebarre, Tom Hubrecht, Christoph Lauter, Jean-Michel Muller, and Kristalys Ruiz-Rohena.
Correctly rounded vector implementation of the exponential function in binary64 arithmetic.
*33rd IEEE International Symposium on Computer Arithmetic*.
Fulda, Germany, 2026.
