Enabling Floating-Point Arithmetic in the Coq Proof Assistant - Assistance à la Certification d’Applications DIstribuées et Embarquées
Preprints, Working Papers, ... Year : 2022

Enabling Floating-Point Arithmetic in the Coq Proof Assistant

Abstract

Floating-point arithmetic is a well-known and extremely efficient way of performing approximate computations over the real numbers. Although it requires some careful considerations, floating-point numbers are nowadays routinely used to prove mathematical theorems. Numerical computations have been applied in the context of formal proofs too, as illustrated by the CoqInterval library. But these computations do not benefit from the powerful floating-point units available in modern processors, since they are emulated inside the logic of the formal system. This paper experiments with the use of hardware floating-point numbers for numerically intensive proofs verified by the Coq proof assistant. This gives rise to various questions regarding the formalization, the implementation, the usability, and the level of trust. This approach has been applied to the CoqInterval and ValidSDP libraries, which demonstrates a speedup of at least one order of magnitude.
Fichier principal
Vignette du fichier
article.pdf (454.25 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04114233 , version 1 (01-06-2023)
hal-04114233 , version 2 (31-08-2023)

Licence

Identifiers

  • HAL Id : hal-04114233 , version 1

Cite

Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux. Enabling Floating-Point Arithmetic in the Coq Proof Assistant. 2022. ⟨hal-04114233v1⟩

Collections

IRIT-UT3
661 View
260 Download

Share

More