522 search results for ""

Showing 451 - 500
  1. coq-unimath-ktheory

    No documentation

    Aims to formalize a substantial body of mathematics using the univalent point of view
    The UniMath Development Team
    0.1.0
    Kind of MIT
    Used by 1 other packages
    14 May 2019
  2. coq-unimath-substitution-systems

    No documentation

    Aims to formalize a substantial body of mathematics using the univalent point of view
    The UniMath Development Team
    0.1.0
    Kind of MIT
    Used by 0 other packages
    14 May 2019
  3. coq-unimath-tactics

    No documentation

    Aims to formalize a substantial body of mathematics using the univalent point of view
    The UniMath Development Team
    0.1.0
    Kind of MIT
    Used by 0 other packages
    14 May 2019
  4. coq-universe-comparator

    No documentation

    A tool to compare universe levels in Coq
    logpath:UniverseComparator
    Amin Timany
    1.1.0
    MIT
    Used by 0 other packages
    25 Nov 2015
  5. coq-validsdp

    No documentation

    ValidSDP
    keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:Miscellaneous/Coq Extensions logpath:ValidSDP
    Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr>
    1.1.0
    LGPL-2.1-or-later
    Used by 0 other packages
    17 Sep 2025
  6. coq-vcfloat

    No documentation

    VCFloat: Floating Point Round-off Error Analysis
    date:2025-02-10 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat
    Andrew W. Appel Ariel E. Kellison Tahina Ramananandro Paul Mountcastle Benoit Meister et al.
    2.3
    LGPL-3.0-or-later
    Used by 2 other packages
    10 Feb 2025
  7. coq-vellvm

    No documentation

    Coq library implementing (executable) semantics for LLVM IR
    date:2025-01-10 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>
    v2.0.20250110
    GPL-3.0-or-later
    Used by 0 other packages
    11 Jan 2025
  8. coq-verified-extraction

    No documentation

    A Verified Extraction from Gallina to OCaml, written in Gallina
    Yannick Forster Matthieu Sozeau Nicolas Tabareau
    0.9.2+8.19
    MIT
    Used by 0 other packages
    23 Jul 2024
  9. coq-vlsm

    No documentation

    Coq formalization of validating labelled state transition and message production systems
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:consensus keyword:fault tolerance keyword:distributed algorithms keyword:Paxos logpath:VLSM date:2023-12-15
    Mihai Calancea Denisa Diaconescu Wojciech Kołowski Elaine Li Brandon Moore et al.
    1.3
    BSD-3-Clause
    Used by 0 other packages
    15 Dec 2023
  10. coq-void

    No documentation

    MathComp instances for the empty type (Empty_set)
    keyword:empty type keyword:class instances category:Computer Science/Data Types and Data Structures date:2019-10-08 logpath:void
    Arthur Azevedo de Amorim
    0.1.0
    MIT
    Used by 0 other packages
    08 Oct 2019
  11. coq-vst

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2025-01-20
    Andrew W. Appel Lennart Beringer William Mansky Josiah Dodds Qinxiang Cao et al.
    3.1beta
    BSD-2-Clause
    Used by 1 other packages
    23 Jun 2025
  12. coq-vst-32

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2024-03-20
    Andrew W. Appel Lennart Beringer Josiah Dodds Qinxiang Cao Aquinas Hobor et al.
    2.14
    BSD-2-Clause
    Used by 0 other packages
    21 Mar 2024
  13. coq-vst-64

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2020-08-02
    Andrew W. Appel Lennart Beringer Sandrine Blazy Qinxiang Cao Santiago Cuellar et al.
    2.6
    https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
    Used by 0 other packages
    03 Aug 2020
  14. coq-vst-iris

    No documentation

    Verified Software Toolchain with Iris
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2023-01-24
    William Mansky Shengyi Wang
    2.11.1
    https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
    Used by 0 other packages
    25 Jan 2023
  15. coq-vst-lib

    No documentation

    VSTlib: VST-verified C library for VST-verified clients
    date:2025-02-10 keyword:VST keyword:library keyword:malloc keyword:threads keyword:floating-point arithmetic category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VSTlib
    Andrew W. Appel William Mansky
    2.15.1
    BSD-2-Clause
    Used by 0 other packages
    10 Feb 2025
  16. coq-vst-ora

    No documentation

    Ordered Resource Algebras for Iris
    Robbert Krebbers Ralf Jung Amin Timany William Mansky
    1.0
    Used by 1 other packages
    12 Jun 2025
  17. coq-vst-zlist

    No documentation

    A list library indexed by Z type, with a powerful automatic solver
    Qinshi Wang Andrew W. Appel
    2.13
    BSD-2-Clause
    Used by 2 other packages
    09 Nov 2023
  18. coq-wasm

    No documentation

    Wasm formalisation in Coq
    keyword:WebAssembly category:Computer Science/Semantics and Compilation/Semantics date:2025-08-20 logpath:Wasm
    Martin Bodin Philippa Gardner Jean Pichon Xiaojia Rao Conrad Watt
    2.2.0
    MIT
    Used by 0 other packages
    25 Aug 2025
  19. coq-waterproof

    No documentation

    Coq proofs in a style that resembles non-mechanized mathematical proofs
    keyword:mathematics education category:Mathematics/Education date:2023-08-27 logpath:Waterproof
    Jelle Wemmenhove Balthazar Pathiachvili Cosmin Manea Lulof Pirée Adrian Vrămuleţ et al.
    2.0.1+8.17
    LGPL-3.0-or-later
    Used by 0 other packages
    27 Aug 2023
  20. coq-weak-up-to

    No documentation

    New Up-to Techniques for Weak Bisimulation
    keyword: weak bisimilarity keyword: weak bisimulation keyword: up-to techniques keyword: termination keyword: commutation keyword: Newman's lemma category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems date: 2005-02-22
    Damien Pous <damien.pous at ens-lyon.fr> [http://perso.ens-lyon.fr/damien.pous/]
    8.10.0
    GPL
    Used by 0 other packages
    07 Dec 2019
  21. coq-yalla

    No documentation

    Yalla library
    keyword:linear logic keyword:metatheory keyword:cut elimination category:Mathematics/Logic/Foundations date:2024-09-16 logpath:Yalla
    Olivier Laurent
    2.0.6
    LGPL-3.0-or-later
    Used by 0 other packages
    16 Sep 2024
  22. coq-zchinese

    No documentation

    A proof of the Chinese Remainder Lemma
    keyword: number theory keyword: chinese remainder keyword: primality keyword: prime numbers category: Mathematics/Arithmetic and Number Theory/Number theory category: Miscellaneous/Extracted Programs/Arithmetic
    Valérie Ménissier-Morain
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  23. coq-zf

    No documentation

    An axiomatisation of intuitionistic Zermelo-Fraenkel set theory
    keyword: set theory keyword: Zermelo-Fraenkel category: Mathematics/Logic/Set theory
    Guillaume Alexandre
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  24. coq-zfc

    No documentation

    An encoding of Zermelo-Fraenkel Set Theory in Coq
    keyword: set theory keyword: Zermelo-Fraenkel keyword: Calculus of Inductive Constructions category: Mathematics/Logic/Set theory
    Benjamin Werner
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  25. coq-zorns-lemma

    No documentation

    This library develops some basic set theory in Coq
    category:Mathematics/Logic/Set theory date:2023-08-18 keyword:set theory keyword:cardinals keyword:ordinal numbers keyword:finite keyword:countable keyword:quotients keyword:well-orders keyword:Zorn's lemma logpath:ZornsLemma
    Daniel Schepler
    10.2.0
    LGPL-2.1-or-later
    Used by 1 other packages
    21 Aug 2023
  26. coq-zsearch-trees

    No documentation

    Binary Search Trees
    keyword: binary search trees category: Computer Science/Data Types and Data Structures category: Miscellaneous/Extracted Programs/Data structures
    Pierre Castéran
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  27. rocq-aac-tactics

    No documentation

    Rocq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
    category:Miscellaneous/Rocq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:reflexive tactic keyword:rewriting keyword:rewriting modulo associativity and commutativity keyword:rewriting modulo ac keyword:decision procedure logpath:AAC_tactics date:2025-10-28
    Thomas Braibant Damien Pous Fabian Kunze
    9.0.0
    LGPL-3.0-or-later
    Used by 0 other packages
    28 Oct 2025
  28. rocq-autosubst-ocaml

    No documentation

    OCaml implementation of Autosubst for Rocq
    Adrian Dapprich
    1.1+9.0
    MIT
    Used by 0 other packages
    17 Apr 2025
  29. rocq-bignums

    No documentation

    Bignums, the Rocq library of arbitrarily large numbers
    category:Miscellaneous/Coq Extensions category:Mathematics/Arithmetic and Number Theory/Number theory category:Mathematics/Arithmetic and Number Theory/Rational numbers keyword:integer numbers keyword:rational numbers keyword:arithmetic keyword:arbitrary-precision logpath:Bignums
    Laurent Théry Benjamin Grégoire Arnaud Spiwack Evgeny Makarov Pierre Letouzey
    9.0.0+rocq9.1
    LGPL-2.1-only
    Used by 1 other packages
    16 Sep 2025
  30. rocq-coinduction

    No documentation

    A library for doing proofs by (enhanced) coinduction
    keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity logpath:Coinduction date:2025-09-17
    Damien Pous <Damien.Pous@ens-lyon.fr>
    1.21
    LGPL-3.0-or-later
    Used by 1 other packages
    19 Sep 2025
  31. rocq-elpi

    No documentation

    Elpi extension language for Coq
    category:Miscellaneous/Coq Extensions keyword:λProlog keyword:higher order abstract syntax logpath:elpi
    Enrico Tassi <enrico.tassi@inria.fr>
    3.2.0
    LGPL-2.1-or-later
    Used by 2 other packages
    19 Sep 2025
  32. rocq-equations

    No documentation

    A function definition package for Rocq
    keyword:dependent pattern-matching keyword:functional elimination category:Miscellaneous/Coq Extensions logpath:Equations
    Matthieu Sozeau <matthieu.sozeau@inria.fr> Cyprien Mangin <cyprien.mangin@m4x.org>
    1.3.1+9.0
    LGPL-2.1-only
    Used by 3 other packages
    20 Mar 2025
  33. rocq-hierarchy-builder

    No documentation

    High level commands to declare and evolve a hierarchy based on packed classes
    logpath:HB
    Cyril Cohen Kazuhiko Sakaguchi Enrico Tassi
    1.10.1
    MIT
    Used by 2 other packages
    08 Sep 2025
  34. 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
  35. 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
  36. 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
  37. 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.4.0
    CECILL-B
    Used by 3 other packages
    15 Apr 2025
  38. 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.4.0
    CECILL-B
    Used by 1 other packages
    15 Apr 2025
  39. 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.4.0
    CECILL-B
    Used by 3 other packages
    15 Apr 2025
  40. 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.4.0
    CECILL-B
    Used by 3 other packages
    15 Apr 2025
  41. 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.1
    CECILL-B
    Used by 2 other packages
    29 Apr 2025
  42. 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
  43. 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.4.0
    CECILL-B
    Used by 3 other packages
    15 Apr 2025
  44. rocq-mathcomp-ssreflect

    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:order theory keyword:partial order keyword:lattices keyword:lists keyword:ordering and sorting lists keyword:prime numbers keyword:tuples keyword:bounded lists logpath:mathcomp.ssreflect
    The Mathematical Components team
    2.4.0
    CECILL-B
    Used by 4 other packages
    15 Apr 2025
  45. 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.4+9.0
    MIT
    Used by 0 other packages
    26 Mar 2025
  46. 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.4+9.0
    MIT
    Used by 2 other packages
    26 Mar 2025
  47. 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.4+9.0
    MIT
    Used by 1 other packages
    26 Mar 2025
  48. 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.4+9.0
    MIT
    Used by 2 other packages
    26 Mar 2025
  49. 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.4+9.0
    MIT
    Used by 3 other packages
    26 Mar 2025
  50. 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.4+9.0
    MIT
    Used by 1 other packages
    26 Mar 2025
... 9 10 11