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.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Primitive Floats in Coq


    Beteiligte:

    Erscheinungsdatum :

    2019-01-01



    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Klassifikation :

    DDC:    004 / 629




    Aircraft floats

    Online Contents | 2011


    Aircraft floats

    Online Contents | 2009


    Flying Floats

    NTIS | 1994


    Aircraft floats

    Online Contents | 2010


    AIRCRAFT FLOATS

    WILLFORD NEAL HERBERT | Europäisches Patentamt | 2021

    Freier Zugriff