12 search results for "tag:"date:2025-06""

Showing 1 - 12
  1. 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:2025-06-11
    Guillaume Melquiond <guillaume.melquiond@inria.fr>
    1.7.1
    LGPL-3.0-or-later
    Used by 0 other packages
    12 Jun 2025
  2. coq-iris

    No documentation

    A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
    date:2025-06-04 logpath:iris.prelude logpath:iris.algebra logpath:iris.si_logic logpath:iris.bi logpath:iris.proofmode logpath:iris.base_logic logpath:iris.program_logic
    The Iris Team
    4.4.0
    BSD-3-Clause
    Used by 2 other packages
    12 Jun 2025
  3. coq-iris-heap-lang

    No documentation

    The canonical example language for Iris
    date:2025-06-04 logpath:iris.heap_lang
    The Iris Team
    4.4.0
    BSD-3-Clause
    Used by 0 other packages
    12 Jun 2025
  4. coq-stdpp

    No documentation

    An extended "Standard Library" for Coq
    date:2025-06-04 logpath:stdpp
    The std++ team
    1.12.0
    BSD-3-Clause
    Used by 4 other packages
    12 Jun 2025
  5. coq-stdpp-bitvector

    No documentation

    A library for bitvectors based on std++
    date:2025-06-04 logpath:stdpp.bitvector
    The std++ team
    1.12.0
    BSD-3-Clause
    Used by 0 other packages
    12 Jun 2025
  6. coq-wasm

    No documentation

    Wasm formalisation in Coq
    keyword:WebAssembly category:Computer Science/Semantics and Compilation/Semantics date:2025-06-29 logpath:Wasm
    Martin Bodin Philippa Gardner Jean Pichon Xiaojia Rao Conrad Watt
    2.1.0
    MIT
    Used by 0 other packages
    30 Jun 2025
  7. rocq-num-analysis-algebra

    No documentation

    Algebraic structures for numerical analysis in Rocq
    category:Math/Algebra date:2025-06 logpath:NumAnalysis.Algebra keyword:algebra keyword:algebraic structure hierarchy keyword:functions to an algebraic structure keyword:algebraic substructure keyword:morphism keyword:monoid keyword:group keyword:ring keyword:module space keyword:affine space keyword:dimension theorem keyword:incomplete basis theorem keyword:dual basis keyword:predual basis keyword:rank-nullity theorem keyword:binomial coefficient
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.0.0
    LGPL-3.0-or-later
    Used by 2 other packages
    23 Jun 2025
  8. rocq-num-analysis-fem

    No documentation

    The finite element method
    category:Math/Real Calculus and Topology date:2025-06 logpath:NumAnalysis.FEM keyword:multi-index keyword:multi-variate polynomial keyword:Lagrange polynomial keyword:finite element keyword:simplicial Lagrange finite element
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.0.0
    LGPL-3.0-or-later
    Used by 1 other packages
    23 Jun 2025
  9. rocq-num-analysis-lax-milgram

    No documentation

    Lax-Milgram theorem
    category:Math/Real Calculus and Topology date:2025-06 logpath:NumAnalysis.LM keyword:fixed point theorem (in a Banach space) keyword:orthogonal projection keyword:orthogonal complement keyword:Riesz-Fréchet representation theorem keyword:Lax-Milgram theorem keyword:Céa's lemma
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.0.0
    LGPL-3.0-or-later
    Used by 1 other packages
    23 Jun 2025
  10. rocq-num-analysis-lebesgue

    No documentation

    Lebesgue integral
    category:Math/Real Calculus and Topology date:2025-06 logpath:NumAnalysis.Lebesgue keyword:sigma-algebra keyword:monotone class theorem keyword:Dynkin pi-lambda theorem keyword:measure theory keyword:Lebesgue measure keyword:simple function keyword:adapted sequence keyword:Beppo Levi (monotone convergence) theorem keyword:Fatou lemma keyword:Lebesgue (dominated convergence) theorem keyword:Lebesgue induction principle keyword:Tonelli theorem keyword:Bochner integral
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.0.0
    LGPL-3.0-or-later
    Used by 1 other packages
    23 Jun 2025
  11. rocq-num-analysis-subset

    No documentation

    Subsets for numerical analysis in Rocq
    category:Math/Logic/Set theory date:2025-06 logpath:NumAnalysis.Requisite logpath:NumAnalysis.Logic logpath:NumAnalysis.Numbers logpath:NumAnalysis.Subsets keyword:subset keyword:function keyword:homogeneous binary relation keyword:operation on finite families
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.0.0
    LGPL-3.0-or-later
    Used by 2 other packages
    23 Jun 2025
  12. rocq-parseque

    No documentation

    Total parser combinators in Rocq/Coq
    category:Computer Science/Data Types and Data Structures date:2025-06-24 logpath:parseque
    G. Allais
    0.3.0
    MIT
    Used by 0 other packages
    27 Jun 2025