279 search results for "tag:"date:""

Showing 251 - 279
  1. rocq-jsast

    No documentation

    A minimal JavaScript syntax tree carved out of the JsCert project
    keyword:javascript keyword:compiler date:2026-02-27 logpath:JsAst
    Martin Bodin <> Arthur Charguéraud <> Daniele Filaretti <> Philippa Gardner <> Sergio Maffeis <> et al.
    4.0.0
    BSD-2-Clause
    Used by 0 other packages
    02 Mar 2026
  2. rocq-laproof

    No documentation

    LAProof: a library of formal proofs of accuracy and correctness for linear algebra programs
    date:2026-09-25 logpath:LAProof
    Ariel E. Kellison Andrew W. Appel Mohit Tekriwal David Bindel
    2.0.1
    MIT
    Used by 0 other packages
    29 Sep 2026
  3. rocq-libhyps

    No documentation

    Hypotheses manipulation library
    keyword:proof environment manipulation keyword:forward reasoning keyword:hypothesis naming category:Miscellaneous/Coq Extensions logpath:LibHyps date:2026-04-13
    Pierre Courtieu
    5.0
    MIT
    Used by 0 other packages
    17 Apr 2026
  4. rocq-listz

    No documentation

    A Rocq library of lists with indices in Z
    date:2026-04-17 logpath:listz
    François Pottier <francois.pottier@inria.fr>
    20260417
    LGPL-2.1-only
    Used by 1 other packages
    17 Apr 2026
  5. rocq-marble

    No documentation

    Data structures based on machine integers and primitive arrays
    date:2026-04-21 logpath:marble
    François Pottier <francois.pottier@inria.fr>
    20260421
    LGPL-2.1-only
    Used by 0 other packages
    22 Apr 2026
  6. rocq-mathcomp-hollight-real-with-N

    No documentation

    HOL-Light definition of real numbers in Rocq using N and MathComp
    logpath:MathComp_HOLLight_Real_With_N date:2025-07-11 category:Mathematics/Arithmetic and Number Theory/Miscellaneous category:Mathematics/Real Numbers keyword:HOL-Light
    https://github.com/Deducteam/mathcomp-hollight-real-with-N/blob/main/AUTHORS.md
    0.0.0
    CeCILL-2.1
    Used by 2 other packages
    02 Oct 2025
  7. rocq-mathcomp-real-closed

    No documentation

    Mathematical Components Library on real closed fields
    keyword:real closed field logpath:mathcomp.real_closed date:2024-12-09
    Cyril Cohen Assia Mahboubi
    2.0.6
    CECILL-B
    Used by 2 other packages
    24 Jul 2026
  8. rocq-monae

    No documentation

    Monads and equational reasoning in Rocq
    keyword:monae keyword:effects keyword:probability keyword:nondeterminism logpath:monae date:2026-09-22
    Reynald Affeldt David Nowak Takafumi Saikawa Jacques Garrigue Ayumu Saito et al.
    0.9.3
    LGPL-2.1-or-later
    Used by 0 other packages
    28 Sep 2026
  9. rocq-num-analysis-algebra

    No documentation

    Algebraic structures for numerical analysis in Rocq
    category:Mathematics/Algebra date:2026-03 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.2.0
    LGPL-3.0-or-later
    Used by 2 other packages
    13 Mar 2026
  10. rocq-num-analysis-fem

    No documentation

    The finite element method
    category:Mathematics/Real Calculus and Topology date:2026-03 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.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    13 Mar 2026
  11. rocq-num-analysis-lax-milgram

    No documentation

    Lax-Milgram theorem
    category:Mathematics/Real Calculus and Topology date:2026-03 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.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    13 Mar 2026
  12. rocq-num-analysis-lebesgue

    No documentation

    Lebesgue integral
    category:Mathematics/Real Calculus and Topology date:2026-03 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.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    13 Mar 2026
  13. rocq-num-analysis-subset

    No documentation

    Subsets for numerical analysis in Rocq
    category:Mathematics/Logic/Set theory date:2026-03 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.2.0
    LGPL-3.0-or-later
    Used by 2 other packages
    13 Mar 2026
  14. rocq-ollibs

    No documentation

    OL libraries
    keyword:standard library keyword:list keyword:permutation keyword:decidable equality keyword:finite multiset category:Mathematics/Combinatorics and Graph Theory date:2025-11-11 logpath:OLlibs
    Olivier Laurent Christophe Lucas
    2.1.1
    LGPL-3.0-or-later
    Used by 0 other packages
    12 Nov 2025
  15. rocq-parseque

    No documentation

    Total parser combinators in Rocq/Coq
    category:Computer Science/Data Types and Data Structures date:2026-06-17 logpath:parseque
    G. Allais
    0.3.1
    MIT
    Used by 1 other packages
    17 Jun 2026
  16. rocq-partial

    No documentation

    A Rocq library for extractable partial functions
    category:Computer Science/Semantics and Compilation/Semantics keyword:partial functions keyword:general recursion keyword:monad keyword:extraction logpath:Partial date:2026-10-08
    Théo Winterhalter <theo.winterhalter@inria.fr> Meven Lennon-Bertand <meven.lennon-bertrand@inria.fr> Kenji Maillard <kenji@maillard.blue>
    0.1
    MIT
    Used by 0 other packages
    08 Oct 2026
  17. rocq-partial-orders

    No documentation

    A library for setoids, partial orders, complete lattices and related structures
    keyword:partial order keyword:setoid keyword:lattice keyword:CPO keyword:Pataraia keyword:BourbakiWitt logpath:PartialOrders date:2026-09-21
    Damien Pous <Damien.Pous@ens-lyon.fr>
    1.1
    LGPL-3.0-or-later
    Used by 1 other packages
    21 Sep 2026
  18. rocq-pi-agm

    No documentation

    Computing thousands or millions of digits of PI with arithmetic-geometric means
    keyword:real analysis keyword:pi category:Mathematics/Real Calculus and Topology logpath:agm date:2020-06-23
    Yves Bertot <yves.bertot@inria.fr>
    1.2.9
    CECILL-B
    Used by 0 other packages
    14 Aug 2025
  19. rocq-pi-leibniz

    No documentation

    Constructive pi for the Rocq constructive Cauchy reals with premise-free rational separation
    keyword:pi keyword:constructive reals keyword:irrationality date:2026-10-15 logpath:pi_leibniz
    Wang Baojun <168888@live.cn> Zhou Zhinong <zrm2000@126.com> Zeng Baiyuan <3052633793@qq.com>
    1.0.0
    LGPL-2.1
    Used by 0 other packages
    20 Oct 2026
  20. rocq-robot-rocq

    No documentation

    Formal Foundations for Modeling Robot Manipulators
    keyword:robotics keyword:3D geometry logpath:robot date:2026-09-07
    Reynald Affeldt, AIST Cyril Cohen, Inria Laurent Théry, Inria
    0.3.3
    LGPL-2.1-or-later
    Used by 0 other packages
    10 Sep 2026
  21. rocq-robust-geometric-predicates

    No documentation

    Machine-checked robust binary64 geometric predicates, sound vs. exact arithmetic
    category:Computer Science/Data Types and Data Structures category:Mathematics/Real Calculus and Topology keyword:robust predicates keyword:geometric keyword:geometric predicates keyword:computational geometry keyword:orientation keyword:floating point keyword:Flocq logpath:NTS.Proofs date:2026-08-24
    NetTopologySuite.Proofs contributors
    0.1.0
    BSD-3-Clause
    Used by 0 other packages
    27 Aug 2026
  22. rocq-rouche-capelli

    No documentation

    A proof for the Rouché–Capelli theorem by rocq-math-comp
    category:Mathematics/Algebra keyword:linear algebra keyword:matrix keyword:rank logpath:RoucheCapelli date:2025-11-05
    Cheng-Hui Weng Reynald Affeldt Jacques Garrigue Takafumi Saikawa
    0.2.0
    MIT
    Used by 0 other packages
    20 Nov 2025
  23. rocq-spatial-algebra

    No documentation

    DE-9IM intersection-matrix algebra and integer orientation-determinant bounds (axiom-free)
    category:Computer Science/Data Types and Data Structures keyword:DE-9IM keyword:spatial relations keyword:GIS keyword:intersection matrix keyword:orientation determinant logpath:NTS.Proofs date:2026-08-24
    NetTopologySuite.Proofs contributors
    0.1.0
    BSD-3-Clause
    Used by 0 other packages
    27 Aug 2026
  24. rocq-spivak

    No documentation

    Spivak calculus, textbook exercises, real analysis, and checked tactics
    keyword:calculus keyword:tactics category:Mathematics/Real Calculus and Topology logpath:Lib logpath:Calculus logpath:ATTAM logpath:Backprop date:2026-10-03
    Sterling Jeppson
    0.1.2
    MIT
    Used by 0 other packages
    20 Oct 2026
  25. rocq-stdpp

    No documentation

    An extended "Standard Library" for Rocq
    date:2026-03-05 logpath:stdpp
    The std++ team
    1.13.0
    BSD-3-Clause
    Used by 5 other packages
    06 Mar 2026
  26. rocq-stdpp-bitvector

    No documentation

    A library for bitvectors based on std++
    date:2026-03-05 logpath:stdpp.bitvector
    The std++ team
    1.13.0
    BSD-3-Clause
    Used by 1 other packages
    06 Mar 2026
  27. rocq-vellvm

    No documentation

    Rocq library implementing (executable) semantics for LLVM IR
    date:2026-07-06 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:semantics keyword:interpreter keyword:LLVM logpath:Vellvm
    Steve Zdancewic <stevez@cis.upenn.edu> Yannick Zakowski <yannick.zakowski@inria.fr> Calvin Beck <hobbes@seas.upenn.edu> Irene Yoon <euisuny@cis.upenn.edu> Gary (Hanxi) Chen <hanxic@seas.upenn.edu>
    v3.0.20260707
    MIT
    Used by 0 other packages
    09 Jul 2026
  28. rocq-vst

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2026-08-24
    Andrew W. Appel Lennart Beringer William Mansky Josiah Dodds Qinxiang Cao et al.
    3.2beta
    BSD-2-Clause
    Used by 0 other packages
    07 Sep 2026
  29. rocq-yalla

    No documentation

    Yalla library
    keyword:linear logic keyword:metatheory keyword:cut elimination category:Mathematics/Logic/Foundations date:2025-03-26 logpath:Yalla
    Olivier Laurent
    2.0.7
    LGPL-3.0-or-later
    Used by 0 other packages
    27 Mar 2025
... 4 5 6