7 search results for "tag:"keyword:floating-point arithmetic""

Showing 1 - 7
  1. coq-flocq

    No documentation

    A formalization of floating-point arithmetic for the Coq system
    keyword:floating-point arithmetic logpath:Flocq date:2024-07-02
    Sylvie Boldo <sylvie.boldo@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>
    4.2.0
    LGPL-3.0-or-later
    Used by 16 other packages
    02 Jul 2024
  2. coq-gappa

    No documentation

    A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
    keyword:floating-point arithmetic keyword:interval arithmetic keyword:decision procedure category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Gappa date:2024-02-08
    Guillaume Melquiond <guillaume.melquiond@inria.fr>
    1.5.5
    LGPL-3.0-or-later
    Used by 0 other packages
    08 Feb 2024
  3. coq-interval

    No documentation

    A Coq tactic for proving bounds on real-valued expressions automatically
    keyword:interval arithmetic keyword:decision procedure keyword:floating-point arithmetic keyword:reflexive tactic keyword:Taylor models category:Mathematics/Real Calculus and Topology category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Interval date:2024-10-21
    Guillaume Melquiond <guillaume.melquiond@inria.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr> Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>
    4.11.1
    CeCILL-C
    Used by 7 other packages
    22 Oct 2024
  4. coq-libvalidsdp

    No documentation

    LibValidSDP
    keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:libValidSDP category:Miscellaneous/Coq Extensions logpath:libValidSDP
    Pierre Roux <pierre.roux@onera.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr>
    1.0.2
    LGPL-2.1-or-later
    Used by 1 other packages
    13 Dec 2023
  5. coq-validsdp

    No documentation

    ValidSDP
    keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:Miscellaneous/Coq Extensions logpath:ValidSDP
    Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr>
    1.0.2
    LGPL-2.1-or-later
    Used by 0 other packages
    13 Dec 2023
  6. coq-vcfloat

    No documentation

    VCFloat: Floating Point Round-off Error Analysis
    date:2024-03-20 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat
    Andrew W. Appel Ariel E. Kellison Tahina Ramananandro Paul Mountcastle Benoit Meister et al.
    2.2
    LGPL-3.0-or-later
    Used by 1 other packages
    21 Mar 2024
  7. coq-vst-lib

    No documentation

    VSTlib: VST-verified C library for VST-verified clients
    date:2024-03-20 keyword:VST keyword:library keyword:malloc keyword:threads keyword:floating-point arithmetic category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VSTlib
    Andrew W. Appel William Mansky
    2.14
    BSD-2-Clause
    Used by 0 other packages
    21 Mar 2024