589 search results for ""

Showing 551 - 589
  1. rocq-monae

    No documentation

    Monads and equational reasoning in Rocq
    keyword:monae keyword:effects keyword:probability keyword:nondeterminism logpath:monae date:2026-04-07
    Reynald Affeldt David Nowak Takafumi Saikawa Jacques Garrigue Ayumu Saito et al.
    0.9.2
    LGPL-2.1-or-later
    Used by 1 other packages
    21 Apr 2026
  2. 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.5.1
    GPL-2.0-or-later
    Used by 1 other packages
    15 Jul 2026
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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 0 other packages
    17 Jun 2026
  11. 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-05-07
    Damien Pous <Damien.Pous@ens-lyon.fr>
    1.0
    LGPL-3.0-or-later
    Used by 1 other packages
    18 May 2026
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. rocq-read-file

    No documentation

    Read files from disk into Rocq primitive values
    Jason Gross
    0.0.2
    MIT
    Used by 0 other packages
    19 May 2026
  18. 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.9.0
    LGPL-3.0-or-later
    Used by 1 other packages
    07 May 2026
  19. 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
  20. 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
  21. 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
  22. 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
  23. 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.2
    BSD-2-Clause
    Used by 0 other packages
    29 Jun 2026
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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 53 other packages
    27 Jul 2026
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. rocq-verified-extraction

    No documentation

    Verified extraction from Rocq to OCaml
    keyword:extraction category:Miscellaneous/Rocq Extensions logpath:VerifiedExtraction
    Yannick Forster Matthieu Sozeau Nicolas Tabareau
    1.0.0+9.1
    MIT
    Used by 0 other packages
    13 Mar 2026
  36. 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
  37. rocq-vst-ora

    No documentation

    Ordered Resource Algebras for Iris
    Robbert Krebbers Ralf Jung Amin Timany William Mansky Ke Du
    1.2.1
    Used by 0 other packages
    26 Aug 2026
  38. 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
  39. strict-order-solver

    No documentation

    Complete solver for strict orders (transitive+irreflexive relations) for Rocq
    Kacper Korban Dario Halilovic Marcin Wojnarowski
    1.0.0
    MIT
    Used by 0 other packages
    13 May 2026
... 10 11 12