Primitive Floats in Coq ; Flottants primitifs en Coq
In: ITP 2019, Interactive Theorem Proving ; https://hal.science/hal-02449191 ; ITP 2019, 2019
Online
Konferenz
Zugriff:
International audience ; Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors. Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers. A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.
Titel: |
Primitive Floats in Coq ; Flottants primitifs en Coq
|
---|---|
Autor/in / Beteiligte Person: | Bertholon, Guillaume ; Martin-Dorel, Érik ; Roux, Pierre ; École normale supérieure - Paris (ENS-PSL) ; Université Paris Sciences et Lettres (PSL) ; Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE) ; Institut de recherche en informatique de Toulouse (IRIT) ; Université Toulouse Capitole (UT Capitole) ; Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J) ; Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3) ; Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP) ; Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI) ; Université Toulouse - Jean Jaurès (UT2J) ; Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3) ; Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole) ; Université de Toulouse (UT) ; DTIS, ONERA, Université de Toulouse Toulouse ; ONERA-PRES Université de Toulouse |
Link: | |
Zeitschrift: | ITP 2019, Interactive Theorem Proving ; https://hal.science/hal-02449191 ; ITP 2019, 2019 |
Veröffentlichung: | HAL CCSD, 2019 |
Medientyp: | Konferenz |
DOI: | 10.4230/LIPIcs.ITP.2019.7 |
Schlagwort: |
|
Sonstiges: |
|