2026-07-22T06:50:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11062 2024-03-06T10:47:16Z ddc:004 open_access

Primitive Floats in Coq Bertholon, Guillaume Martin-Dorel, Érik Roux, Pierre Coq formal proofs floating-point arithmetic reflexive tactics Cholesky decomposition 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Guillaume Bertholon and Érik Martin-Dorel and Pierre Roux 2019 Is Part Of LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2019.7 urn:nbn:de:0030-drops-110629 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.7 eng https://creativecommons.org/licenses/by/3.0/legalcode