605 search results for ""

Showing 551 - 600
  1. 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.2
    MIT
    Used by 4 other packages
    16 Jun 2026
  2. 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.2
    MIT
    Used by 1 other packages
    16 Jun 2026
  3. 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.2
    MIT
    Used by 3 other packages
    16 Jun 2026
  4. 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.2
    MIT
    Used by 2 other packages
    16 Jun 2026
  5. 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.2
    MIT
    Used by 4 other packages
    16 Jun 2026
  6. 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.2
    MIT
    Used by 5 other packages
    16 Jun 2026
  7. 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.2
    MIT
    Used by 1 other packages
    16 Jun 2026
  8. 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.2
    MIT
    Used by 3 other packages
    16 Jun 2026
  9. rocq-micromega-plugin

    No documentation

    Micromega plugin for Rocq
    category:Miscellaneous/Rocq Extensions keyword:micromega logpath:micromega-plugin
    Frederic Besson
    1.1.1
    LGPL-2.1
    Used by 1 other packages
    24 Jul 2026
  10. rocq-mltac2

    No documentation

    Ltac2 APIs in OCaml
    Dario Halilovic Pierre-Marie Pédrot
    1.0.0
    LGPL-2.1-only
    Used by 1 other packages
    20 Oct 2026
  11. 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
  12. rocq-navi

    No documentation

    Extension of coq2html Document Generator
    category:Tools/Document Generator keyword:document keyword:html
    Xavier Leroy Reynald Affeldt <reynald.affeldt@aist.go.jp> Yoshihiro Imai <y.imai@aist.go.jp>
    0.6.0
    GPL-2.0-or-later
    Used by 1 other packages
    11 Sep 2026
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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-11-01
    Damien Pous <Damien.Pous@ens-lyon.fr>
    1.2
    LGPL-3.0-or-later
    Used by 1 other packages
    02 Nov 2026
  23. 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
  24. 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
  25. 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
  26. rocq-print-assumptions-json

    No documentation

    Structured JSON output for Print Assumptions
    Jason Gross
    0.0.1
    MIT
    Used by 0 other packages
    27 Jul 2026
  27. 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
  28. 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
  29. rocq-read-file

    No documentation

    Read files from disk into Rocq primitive values
    Jason Gross
    0.0.3
    MIT
    Used by 3 other packages
    20 Oct 2026
  30. 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 date:2026-11-01
    Damien Pous <Damien.Pous@ens-lyon.fr> Christian Doczkal <christian.doczkal@ens-lyon.fr>
    1.9.2
    LGPL-3.0-or-later
    Used by 1 other packages
    02 Nov 2026
  31. 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
  32. 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
  33. 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
  34. rocq-rust-extraction

    No documentation

    Rocq extraction to Rust
    keyword:rust keyword:extraction logpath:TypedExtraction
    The COBRA team
    0.2.1
    MIT
    Used by 3 other packages
    13 Mar 2026
  35. rocq-sail-stdpp

    No documentation

    Support library for Sail, a language for describing the instruction semantics of processors, using stdpp bitvectors
    logpath:Sail category:Computer Science/Semantics and Compilation/Semantics
    Alasdair Armstrong Thomas Bauereiss Brian Campbell Shaked Flur Jonathan French et al.
    0.20.3
    BSD-2-Clause
    Used by 0 other packages
    28 Sep 2026
  36. rocq-semantics

    No documentation

    A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation
    category:Computer Science/Semantics and Compilation/Semantics keyword:natural semantics keyword:denotational semantics keyword:axiomatic semantics keyword:Hoare logic keyword:Dijkstra weakest pre-condition calculus keyword:abstract interpretation keyword:intervals logpath:Semantics
    Yves Bertot
    9.0.0
    MIT
    Used by 0 other packages
    17 Feb 2026
  37. rocq-sims

    No documentation

    A library of various strong and weak simulation relations
    category:Computer Science/Semantics and Compilation/Semantics category:Computer Science/Semantics and Compilation/Compilation keyword:simulation keyword:coinduction up-to logpath:Sims
    Nicolas Chappe
    0.2
    LGPL-3.0-or-later
    Used by 0 other packages
    27 Nov 2025
  38. rocq-smpl

    No documentation

    Smpl: An Extensible Tactic for Coq
    Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de> Yannick Forster <forster@cs.uni-saarland.de> Fabian Kunze <fabian.kunze@cs.uni-saarland.de> Kenji Maillard <kenji.maillard@inria.fr>
    9.0
    MIT
    Used by 0 other packages
    05 Sep 2025
  39. rocq-smt-lib

    No documentation

    Rocq mechanisation of SMT-LIB
    date:2026-10-28 logpath:SMTLIB category:Computer Science/Semantics and Compilation/Semantics keyword:SMT-LIB keyword:SMT
    Shiva Tamil Kumaran Andreas Lööw Philippa Gardner
    1.0
    MIT
    Used by 0 other packages
    29 Oct 2026
  40. 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
  41. 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
  42. rocq-stdlib

    No documentation

    The Rocq Proof Assistant -- Standard Library
    The Rocq development team, INRIA, CNRS, and contributors
    9.2.0
    LGPL-2.1-only
    Used by 66 other packages
    27 Jul 2026
  43. 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 9 other packages
    06 Mar 2026
  44. 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 3 other packages
    06 Mar 2026
  45. rocq-sulfur

    No documentation

    A Rocq plugin to automate reasoning about languages with binders
    keyword:binders keyword:substitution category:Miscellaneous/Rocq Extensions logpath:Sulfur date:2026-10-19
    Mathis Bouverot-Dupuis Thiago Felicissimo Théa Hervier Kenji Maillard Kathrin Stark et al.
    0.1
    MIT
    Used by 0 other packages
    23 Oct 2026
  46. rocq-taylor-rocqs

    No documentation

    A Taylor-series solver for analytic ODEs, verified in Rocq
    keyword:ordinary differential equations keyword:analytic functions keyword:Taylor series keyword:exact real arithmetic keyword:interval arithmetic logpath:TR
    Holger Thies
    1.1
    MIT
    Used by 0 other packages
    23 Sep 2026
  47. rocq-typed-extraction

    No documentation

    Rocq extraction to Rust and Elm
    keyword:extraction logpath:TypedExtraction
    The COBRA team
    0.2.1
    MIT
    Used by 0 other packages
    13 Mar 2026
  48. rocq-typed-extraction-common

    No documentation

    Rocq extraction to Rust and Elm
    keyword:extraction logpath:TypedExtraction
    The COBRA team
    0.2.1
    MIT
    Used by 2 other packages
    13 Mar 2026
  49. rocq-typed-extraction-plugin

    No documentation

    Rocq extraction to Rust and Elm
    keyword:extraction logpath:TypedExtraction
    The COBRA team
    0.2.1
    MIT
    Used by 1 other packages
    13 Mar 2026
  50. 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
... 11 12 13