565 search results for ""

Showing 501 - 550
  1. rocq-hollight-logic

    No documentation

    HOL-Light library necessary for translating unify
    logpath:HOLLight_Logic date:2025-10-21 keyword:HOL-Light keyword:first order logic
    Antoine Gontard
    0.0.0
    CeCILL-2.1
    Used by 0 other packages
    25 Oct 2025
  2. rocq-hollight-logic-unif

    No documentation

    HOL-Light library necessary for translating unify
    logpath:HOLLight_Logic_fole date:2025-10-16 keyword:HOL-Light keyword:first order logic
    Antoine Gontard
    0.0.0
    CeCILL-2.1
    Used by 1 other packages
    22 Oct 2025
  3. rocq-iris

    No documentation

    A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
    date:2026-03-05 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.5.0
    BSD-3-Clause
    Used by 1 other packages
    06 Mar 2026
  4. rocq-iris-heap-lang

    No documentation

    The canonical example language for Iris
    date:2026-03-05 logpath:iris.heap_lang
    The Iris Team
    4.5.0
    BSD-3-Clause
    Used by 0 other packages
    06 Mar 2026
  5. 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
  6. rocq-lean-import

    No documentation

    Plugin allowing Rocq to import Lean exported files
    logpath:LeanImport
    Gaëtan Gilbert
    0.0.1
    LGPL-2.1-only
    Used by 0 other packages
    10 Dec 2025
  7. rocq-libhyps

    No documentation

    Hypotheses manipulation library
    keyword:proof environment manipulation keyword:forward reasoning keyword:hypothesis naming category:Miscellaneous/Coq Tactics Library logpath:LibHyps date:2025-10-6
    Pierre Courtieu
    4.0
    MIT
    Used by 0 other packages
    14 Oct 2025
  8. rocq-mathcomp-algebra

    No documentation

    Mathematical Components Library on Algebra
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:algebraic structure hierarchies keyword:archimedean field keyword:floor keyword:ceil keyword:intervals keyword:matrices keyword:vectors keyword:block matrices keyword:determinant keyword:Cramer rule keyword:Vandermonde matrices keyword:LUP decomposition keyword:Gaussian elimination keyword:matrix rank keyword:eigen values keyword:single variable polynomials keyword:bivariate polynomials keyword:polynomial division keyword:integers keyword:rational numbers keyword:semirings keyword:rings keyword:left algebra keyword:left module keyword:unit rings keyword:field keyword:algebraically closed field keyword:additive morphisms keyword:ring morphisms keyword:finite dimensional vector spaces keyword:complex numbers keyword:square root logpath:mathcomp.algebra
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 7 other packages
    13 Nov 2025
  9. 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
  10. 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
  11. rocq-mathcomp-bigenough

    No documentation

    A small library to do epsilon - N reasoning
    keyword:bigenough keyword:asymptotic reasonning keyword:small scale reflection keyword:mathematical components logpath:mathcomp.bigenough
    Cyril Cohen
    1.0.4
    CeCILL-B
    Used by 3 other packages
    23 Feb 2026
  12. rocq-mathcomp-boot

    No documentation

    Small Scale Reflection
    keyword:small scale reflection keyword:mathematical components keyword:bigop keyword:big operators keyword:biomial coefficient keyword:integer division theory keyword:finite sets keyword:functions with finite domain keyword:finite graphs keyword:quotient types keyword:lists keyword:ordering and sorting lists keyword:prime numbers keyword:tuples keyword:bounded lists logpath:mathcomp.boot
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 8 other packages
    13 Nov 2025
  13. rocq-mathcomp-character

    No documentation

    Mathematical Components Library on character theory
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:character logpath:mathcomp.character
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 1 other packages
    13 Nov 2025
  14. 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
  15. 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
  16. rocq-mathcomp-field

    No documentation

    Mathematical Components Library on Fields
    keyword:small scale reflection keyword:mathematical components keyword:algebra keyword:field logpath:mathcomp.field
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 4 other packages
    13 Nov 2025
  17. rocq-mathcomp-fingroup

    No documentation

    Mathematical Components Library on finite groups
    keyword:small scale reflection keyword:mathematical components keyword:finite groups logpath:mathcomp.fingroup
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 4 other packages
    13 Nov 2025
  18. rocq-mathcomp-finmap

    No documentation

    Finite sets, finite maps, finitely supported functions
    keyword:finmap keyword:finset keyword:multiset logpath:mathcomp.finmap
    Cyril Cohen Kazuhiko Sakaguchi
    2.2.2
    CECILL-B
    Used by 3 other packages
    13 Nov 2025
  19. 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
  20. rocq-mathcomp-order

    No documentation

    Mathematical Components Library on order theory
    keyword:small scale reflection keyword:mathematical components keyword:order theory keyword:partial order keyword:lattices keyword:total order logpath:mathcomp.order
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 6 other packages
    13 Nov 2025
  21. 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
  22. 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
  23. rocq-mathcomp-solvable

    No documentation

    Mathematical Components Library on finite groups (II)
    keyword:small scale reflection keyword:mathematical components keyword:finite groups logpath:mathcomp.solvable
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 4 other packages
    13 Nov 2025
  24. rocq-mathcomp-ssreflect

    No documentation

    Compatibility package for rocq-mathcomp-boot and rocq-mathcomp-order
    The Mathematical Components team
    2.5.0
    CECILL-B
    Used by 4 other packages
    13 Nov 2025
  25. rocq-metarocq

    No documentation

    A meta-programming framework for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 0 other packages
    12 Mar 2026
  26. rocq-metarocq-common

    No documentation

    The common library of Template Rocq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  27. rocq-metarocq-erasure

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  28. rocq-metarocq-erasure-plugin

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  29. rocq-metarocq-pcuic

    No documentation

    A type system equivalent to Rocq's and its metatheory
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  30. rocq-metarocq-quotation

    No documentation

    Gallina quotation functions for Template Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 1 other packages
    12 Mar 2026
  31. rocq-metarocq-safechecker

    No documentation

    Implementation and verification of safe conversion and typechecking algorithms for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  32. rocq-metarocq-safechecker-plugin

    No documentation

    Implementation and verification of an erasure procedure for Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 2 other packages
    12 Mar 2026
  33. rocq-metarocq-template

    No documentation

    A quoting and unquoting library for Rocq in Rocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 4 other packages
    12 Mar 2026
  34. rocq-metarocq-template-pcuic

    No documentation

    Translations between Template Rocq and PCUIC and proofs of correctness
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 5 other packages
    12 Mar 2026
  35. rocq-metarocq-translations

    No documentation

    Translations built on top of MetaRocq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 1 other packages
    12 Mar 2026
  36. rocq-metarocq-utils

    No documentation

    The utility library of Template Rocq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.5.1+9.1
    MIT
    Used by 3 other packages
    12 Mar 2026
  37. rocq-navi

    No documentation

    Extension of coq2html Document Generator
    category:Tools/Document Generator keyword:document keyword:html logpath:
    Xavier Leroy Reynald Affeldt <reynald.affeldt@aist.go.jp> Yoshihiro Imai <y.imai@aist.go.jp>
    0.4.1
    GPL-2.0-or-later
    Used by 0 other packages
    18 Mar 2026
  38. rocq-num-analysis

    No documentation

    Numerical analysis in Rocq
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    2.2.0
    LGPL-3.0-or-later
    Used by 0 other packages
    13 Mar 2026
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. rocq-primitive

    No documentation

    Rocq primitive object OCaml library
    The Rocq development team, INRIA, CNRS, and contributors
    9.0.0
    LGPL-2.1-only
    Used by 0 other packages
    26 Jan 2026
  48. 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
  49. 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
  50. rocq-relation-algebra

    No documentation

    Relation Algebra and KAT in Rocq
    keyword:relation algebra keyword:Kleene algebra with tests keyword:KAT keyword:allegories keyword:residuated structures keyword:automata keyword:regular expressions keyword:matrices category:Mathematics/Algebra logpath:RelationAlgebra
    Damien Pous <Damien.Pous@ens-lyon.fr> Christian Doczkal <christian.doczkal@ens-lyon.fr>
    1.8.0
    LGPL-3.0-or-later
    Used by 1 other packages
    19 Sep 2025
... 10 11 12