21 search results for "author:"Pierre Roux""

Showing 1 - 21
  1. coq-coqeal

    No documentation

    CoqEAL - The Coq Effective Algebra Library
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:effective algebra keyword:elementary divisor rings keyword:Smith normal form keyword:mathematical components keyword:Bareiss keyword:Karatsuba multiplication keyword:refinements logpath:CoqEAL
    Guillaume Cano Cyril Cohen Maxime Dénès Érik Martin-Dorel Anders Mörtberg et al.
    2.1.1
    MIT
    Used by 4 other packages
    08 Dec 2025
  2. 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:2026-02-23
    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.4
    CeCILL-C
    Used by 8 other packages
    23 Feb 2026
  3. coq-libvalidsdp

    No documentation

    LibValidSDP
    keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:Miscellaneous/Coq Extensions logpath:libValidSDP
    Pierre Roux <pierre.roux@onera.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr>
    1.1.1
    LGPL-2.1-or-later
    Used by 1 other packages
    13 Nov 2025
  4. coq-mathcomp-algebra-tactics

    No documentation

    Ring, field, lra, nra, and psatz tactics for Mathematical Components
    logpath:mathcomp.algebra_tactics
    Kazuhiko Sakaguchi Pierre Roux
    1.2.7
    CECILL-B
    Used by 3 other packages
    05 Sep 2025
  5. coq-mathcomp-analysis

    No documentation

    Compatibility package for rocq-mathcomp-analysis
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 7 other packages
    16 Mar 2026
  6. coq-mathcomp-analysis-stdlib

    No documentation

    Compatibility package for rocq-mathcomp-analysis-stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 0 other packages
    16 Mar 2026
  7. coq-mathcomp-classical

    No documentation

    Compatibility package for rocq-mathcomp-classical
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 4 other packages
    16 Mar 2026
  8. coq-mathcomp-dioid

    No documentation

    Dioid
    keyword:dioid keyword:semiring keyword:complete dioid category:Miscellaneous/Coq Extensions logpath:mathcomp.dioid
    Lucien Rakotomalala <lucien.rakotomalala@onera.fr> Pierre Roux <pierre.roux@onera.fr>
    0.2
    CECILL-B
    Used by 0 other packages
    20 Dec 2021
  9. coq-mathcomp-experimental-reals

    No documentation

    Compatibility package for rocq-mathcomp-experimental-reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 1 other packages
    16 Mar 2026
  10. coq-mathcomp-reals

    No documentation

    Compatibility package for rocq-mathcomp-reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 0 other packages
    16 Mar 2026
  11. coq-mathcomp-reals-stdlib

    No documentation

    Compatibility package for rocq-mathcomp-reals-stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 4 other packages
    16 Mar 2026
  12. coq-paramcoq

    No documentation

    Plugin for generating parametricity statements to perform refinement proofs
    keyword:paramcoq keyword:parametricity keyword:OCaml modules category:Miscellaneous/Rocq Extensions logpath:Param date:2024-06-29
    Chantal Keller (Inria, École polytechnique) Marc Lasson (ÉNS de Lyon) Abhishek Anand Pierre Roux Emilio Jesús Gallego Arias et al.
    1.1.3+rocq9.0
    MIT
    Used by 4 other packages
    26 Mar 2025
  13. 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.1.1
    LGPL-2.1-or-later
    Used by 0 other packages
    13 Nov 2025
  14. rocq-mathcomp-analysis

    No documentation

    An analysis library for mathematical components
    category:Mathematics/Real Calculus and Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:Landau notation keyword:logarithm keyword:sin keyword:cos keyword:tangent keyword:trigonometric function keyword:exponential keyword:differentiation keyword:derivative keyword:measure theory keyword:integration keyword:Lebesgue keyword:probability logpath:mathcomp.analysis
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 2 other packages
    16 Mar 2026
  15. rocq-mathcomp-analysis-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers category:Mathematics/Real Calculus and Topology keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 1 other packages
    16 Mar 2026
  16. rocq-mathcomp-classical

    No documentation

    A library for classical logic for mathematical components
    category:Mathematics/Logic/Classical logic keyword:classical logic keyword:logic keyword:sets keyword:set theory keyword:function keyword:cardinal keyword:filter logpath:mathcomp.classical
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 2 other packages
    16 Mar 2026
  17. rocq-mathcomp-experimental-reals

    No documentation

    A library for alternative real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.experimental_reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 1 other packages
    16 Mar 2026
  18. rocq-mathcomp-reals

    No documentation

    A library for real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals keyword:extended real numbers logpath:mathcomp.reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 4 other packages
    16 Mar 2026
  19. rocq-mathcomp-reals-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.16.0
    CECILL-C
    Used by 2 other packages
    16 Mar 2026
  20. rocq-prosa

    No documentation

    A Foundation for Formally Proven Schedulability Analysis
    keyword:prosa keyword:real-time keyword:schedulability analysis keyword:response-time analysis keyword:scheduling theory logpath:prosa
    Felipe Cerqueira Sergey Bozhko Björn Brandenburg Pierre Roux Kimaya Bedarkar et al.
    0.6
    BSD-2-Clause
    Used by 1 other packages
    31 Oct 2025
  21. rocq-prosa-refinements

    No documentation

    Refinements of Prosa RTAs used by POET
    keyword:prosa keyword:poet keyword:real-time keyword:response-time analysis keyword:scheduling theory logpath:prosa.refinements
    Marco Maida Sergey Bozhko Pierre Roux Björn Brandenburg
    0.6
    BSD-2-Clause
    Used by 0 other packages
    31 Oct 2025