522 search results for ""

Showing 151 - 200
  1. coq-gaia-numbers

    No documentation

    Implementation of the sets of numbers Z, Q, and R following Bourbaki's Elements of Mathematics in Coq
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:integers keyword:rational numbers keyword:real numbers logpath:gaia.numbers date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 0 other packages
    11 Aug 2024
  2. coq-gaia-ordinals

    No documentation

    Implementation and properties of ordinals in Coq using Mathematical Components
    category:Mathematics/Logic/Set theory category:Mathematics/Arithmetic and Number Theory/Number theory keyword:ordered sets keyword:ordinal arithmetic keyword:ordinal numbers keyword:cardinal numbers logpath:gaia.ordinals date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 1 other packages
    11 Aug 2024
  3. coq-gaia-schutte

    No documentation

    Implementation of ordinals in Coq following Schütte and Ackermann
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:ordinal arithmetic keyword:ordinal numbers logpath:gaia.schutte date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 1 other packages
    11 Aug 2024
  4. coq-gaia-stern

    No documentation

    Properties of Fibonacci numbers and the Stern diatomic sequence in Coq
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:Stern-Brocot keyword:fibonacci numbers logpath:gaia.stern date:2024-07-24
    José Grimm Alban Quadrat
    2.2
    MIT
    Used by 0 other packages
    11 Aug 2024
  5. coq-gaia-theory-of-sets

    No documentation

    Implementation of the Theory of Sets from Bourbaki's Elements of Mathematics in Coq
    category:Mathematics/Logic/Set theory keyword:Bourbaki keyword:set theory logpath:gaia.sets date:2024-07-24
    José Grimm Alban Quadrat Carlos Simpson
    2.2
    MIT
    Used by 2 other packages
    11 Aug 2024
  6. coq-games

    No documentation

    A library for algorithmic game theory in Ssreflect/Coq
    category:Mathematics/Combinatorics and Graph Theory keyword:game theory logpath:Games
    Alexander Bagnall Samuel Merten Gordon Stewart
    0.1.0
    BSD-2-Clause
    Used by 0 other packages
    29 Feb 2020
  7. coq-gappa

    No documentation

    A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover
    keyword:floating-point arithmetic keyword:interval arithmetic keyword:decision procedure category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Gappa date:2025-06-11
    Guillaume Melquiond <guillaume.melquiond@inria.fr>
    1.7.1
    LGPL-3.0-or-later
    Used by 0 other packages
    12 Jun 2025
  8. coq-gc

    No documentation

    Formal Verification of an Incremental Garbage Collector
    keyword: Linear temporal logic keyword: finite sets keyword: co-induction keyword: garbage collection category: Computer Science/Semantics and Compilation/Compilation date: 2003-05-9
    Solange Coupet-Grimal and Catherine Nouvet
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  9. coq-generic-environments

    No documentation

    Generic Environments is a library that provides an abstract data type for environments
    category:Mathematics/Logic/Type theory keyword:generic environments keyword:typing keyword:type theory logpath:GenericEnvironments
    Emmanuel Polonowski <emmanuel.polonowski@u-pec.fr>
    8.11.0
    MIT
    Used by 0 other packages
    26 Oct 2020
  10. coq-geocoq

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:neutral geometry keyword:Euclidean geometry keyword:hyperbolic geometry keyword:foundations keyword:Tarski keyword:Hilbert keyword:Euclid keyword:Elements keyword:Pappus keyword:Desargues keyword:arithmetization keyword:Pythagoras keyword:Thales' intercept theorem keyword:continuity keyword:ruler and compass keyword:parallel postulates keyword:model keyword:counter-model keyword:Cartesian space keyword:automation date:2024-03-24
    Michael Beeson <profbeeson@gmail.com> Gabriel Braun <gabriel.braun@unistra.fr> Pierre Boutry <contact@pierre.boutry.fr> Cyril Cohen <cyril.cohen@inria.fr> Charly Gries <charly.gries@etu.unistra.fr> et al.
    2.5.0
    LGPL-3.0-only
    Used by 0 other packages
    25 Mar 2024
  11. coq-geocoq-algebraic

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:Euclidean geometry keyword:hyperbolic geometry keyword:foundations keyword:Tarski keyword:parallel postulates keyword:model keyword:counter-model keyword:Cartesian space date:2024-03-24
    Pierre Boutry <contact@pierre.boutry.fr> Cyril Cohen <cyril.cohen@inria.fr> Stéphane Kastenbaum <stephane.kastenbaum@gmail.com>
    2.5.0
    LGPL-3.0-only
    Used by 2 other packages
    25 Mar 2024
  12. coq-geocoq-axioms

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:neutral geometry keyword:Euclidean geometry keyword:foundations keyword:Tarski keyword:Hilbert keyword:Euclid keyword:Elements keyword:parallel postulates date:2024-03-24
    Michael Beeson <profbeeson@gmail.com> Gabriel Braun <gabriel.braun@unistra.fr> Pierre Boutry <contact@pierre.boutry.fr> Charly Gries <charly.gries@etu.unistra.fr> Julien Narboux <narboux@unistra.fr> et al.
    2.5.0
    LGPL-3.0-only
    Used by 2 other packages
    25 Mar 2024
  13. coq-geocoq-coinc

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:automation date:2024-03-24
    Pierre Boutry <contact@pierre.boutry.fr> Julien Narboux <narboux@unistra.fr> Pascal Schreck <schreck@unistra.fr>
    2.5.0
    LGPL-3.0-only
    Used by 1 other packages
    25 Mar 2024
  14. coq-geocoq-elements

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:neutral geometry keyword:Euclidean geometry keyword:foundations keyword:Euclid keyword:Elements date:2024-03-24
    Michael Beeson <profbeeson@gmail.com> Julien Narboux <narboux@unistra.fr> Freek Wiedijk <freek@cs.ru.nl>
    2.5.0
    LGPL-3.0-only
    Used by 1 other packages
    25 Mar 2024
  15. coq-geocoq-main

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:neutral geometry keyword:Euclidean geometry keyword:foundations keyword:Tarski keyword:Hilbert keyword:Euclid keyword:Pappus keyword:Desargues keyword:arithmetization keyword:Pythagoras keyword:Thales' intercept theorem keyword:continuity keyword:ruler and compass keyword:parallel postulates date:2024-03-24
    Gabriel Braun <gabriel.braun@unistra.fr> Pierre Boutry <contact@pierre.boutry.fr> Charly Gries <charly.gries@etu.unistra.fr> Julien Narboux <narboux@unistra.fr> Pascal Schreck <schreck@unistra.fr>
    2.5.0
    LGPL-3.0-only
    Used by 1 other packages
    25 Mar 2024
  16. coq-geocoq-pof

    No documentation

    A formalization of foundations of geometry in Coq
    category:Mathematics/Geometry/General keyword:geometry keyword:Euclidean geometry keyword:hyperbolic geometry keyword:foundations keyword:Tarski keyword:parallel postulates keyword:model keyword:counter-model keyword:Cartesian space date:2024-03-24
    Pierre Boutry <contact@pierre.boutry.fr> Cyril Cohen <cyril.cohen@inria.fr> Stéphane Kastenbaum <stephane.kastenbaum@gmail.com>
    2.5.0
    LGPL-3.0-only
    Used by 0 other packages
    25 Mar 2024
  17. coq-geometric-algebra

    No documentation

    Grassman Cayley and Clifford formalisations
    logpath:GeometricAlgebra
    Laurent Théry
    0.8.12
    LGPL-2.1-only
    Used by 0 other packages
    27 Aug 2020
  18. coq-giskard

    No documentation

    Verified model of the Giskard consensus protocol in Coq
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:Giskard keyword:consensus keyword:blockchain logpath:Giskard date:2022-11-23
    Elaine Li Karl Palmskog Mircea Sebe
    1.1
    NCSA
    Used by 0 other packages
    21 Jun 2023
  19. coq-goedel

    No documentation

    Coq proof of the Gödel-Rosser 1st incompleteness theorem
    category:Mathematics/Logic/Foundations keyword:Goedel keyword:Rosser keyword:incompleteness keyword:logic keyword:Hilbert logpath:Goedel date:2021-08-10
    Russell O'Connor
    8.13.0
    MIT
    Used by 0 other packages
    10 Aug 2021
  20. coq-graph-basics

    No documentation

    a Coq toolkit for graph theory
    keyword: graph theory keyword: Curry-Howard's isomorphism keyword: inductive definitions category: Mathematics/Combinatorics and Graph Theory date: April 2001
    Jean Duprat
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  21. coq-graph-theory

    No documentation

    General graph theory definitions and results in Coq and MathComp
    category:Computer Science/Graph Theory keyword:graph theory keyword:minors keyword:treewidth keyword:algebra logpath:GraphTheory.core date:2024-06-30
    Christian Doczkal Damien Pous
    0.9.6
    CECILL-B
    Used by 1 other packages
    10 May 2025
  22. coq-graph-theory-planar

    No documentation

    Graph theory results on planarity in Coq and MathComp
    category:Computer Science/Graph Theory keyword:graph theory keyword:planarity logpath:GraphTheory.planar date:2024-06-30
    Christian Doczkal Damien Pous
    0.9.6
    CECILL-B
    Used by 0 other packages
    10 May 2025
  23. coq-graph2tac

    No documentation

    Graph neural network that predicts tactics for Tactician
    Jason Rute Mirek Olsak Lasse Blaauwbroek Fidel I. Schaposnik Massolo Jelle Piepenbrock et al.
    1.0.anon
    https://zenodo.org/records/10410474/files/LICENSE.md
    Used by 0 other packages
    11 Jan 2024
  24. coq-graphs

    No documentation

    Satisfiability of inequality constraints and detection of cycles with negative weight in graphs
    keyword: graphs keyword: graph theory keyword: cycle detection keyword: paths keyword: constraints keyword: inequalities keyword: reflection category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category: Miscellaneous/Extracted Programs/Combinatorics
    Jean Goubault
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  25. coq-ground

    No documentation

    Ground : A Useful Extension to Coq's Standard Library
    Joan Thibault <joan.thibault@ens-rennes.fr>
    0.01.0
    LGPL-3.0-only with OCaml-LGPL-linking-exception
    Used by 0 other packages
    19 Dec 2021
  26. coq-group-theory

    No documentation

    Elements of Group Theory
    keyword: Group Theory category: Mathematics/Algebra
    Gilles Kahn
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  27. coq-groups

    No documentation

    An exercise on groups
    keyword: group theory category: Miscellaneous/Coq Use Examples
    Pierre Castéran
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  28. coq-hammer

    No documentation

    General-purpose automated reasoning hammer tool for Coq
    category:Miscellaneous/Coq Extensions keyword:automation keyword:hammer logpath:Hammer.Plugin date:2025-10-04
    Lukasz Czajka <lukaszcz@mimuw.edu.pl> Cezary Kaliszyk <cezary.kaliszyk@uibk.ac.at>
    1.3.2+9.0
    LGPL-2.1-only
    Used by 1 other packages
    14 Oct 2025
  29. coq-hammer-tactics

    No documentation

    Reconstruction tactics for the hammer for Coq
    keyword:automation keyword:hammer keyword:tactics logpath:Hammer.Tactics date:2025-10-04
    Lukasz Czajka <lukaszcz@mimuw.edu.pl>
    1.3.2+9.0
    LGPL-2.1-only
    Used by 1 other packages
    14 Oct 2025
  30. coq-hanoi

    No documentation

    Hanoi tower in Coq
    keyword:hanoi tower logpath:hanoi
    Laurent Théry
    1.0.0
    MIT
    Used by 0 other packages
    20 Jan 2022
  31. coq-hardware

    No documentation

    Verification and synthesis of hardware linear arithmetic structures
    keyword: hardware verification keyword: comparator circuit category: Computer Science/Architecture category: Miscellaneous/Extracted Programs/Hardware
    Solange Coupet-Grimal & Line Jakubiec
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  32. coq-haskell

    No documentation

    A library to provide Haskell-familiar constructions in Coq
    keyword:haskell category:Miscellaneous/Coq Extensions date:2022-07-22 logpath:Hask
    John Wiegley
    1.1.0
    BSD-3-Clause
    Used by 1 other packages
    22 Jul 2022
  33. coq-hedges

    No documentation

    Some properties of hedges used by hedged bisimulation
    keyword: bisimulation keyword: spi-calculus keyword: hedges category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems date: 20 April 2004
    Sébastien Briais
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  34. coq-hierarchy-builder

    No documentation

    Compatibility package for rocq-hierarchy-builder
    Cyril Cohen Kazuhiko Sakaguchi Enrico Tassi
    1.10.1
    MIT
    Used by 12 other packages
    08 Sep 2025
  35. coq-hierarchy-builder-shim

    No documentation

    Shim package for HB
    logpath:HB
    Cyril Cohen Kazuhiko Sakaguchi Enrico Tassi
    1.6.0
    MIT
    Used by 0 other packages
    20 Sep 2023
  36. coq-high-school-geometry

    No documentation

    Geometry in Coq for French high school
    category:Mathematics/Geometry/General keyword:geometry keyword:teaching keyword:high school keyword:Ptolemy's theorem logpath:HighSchoolGeometry date:2023-11-18
    Frédérique Guilhot Tuan-Minh Pham
    8.16.0
    LGPL-2.1-or-later
    Used by 0 other packages
    18 Nov 2023
  37. coq-higman-cf

    No documentation

    A direct constructive proof of Higman's Lemma
    keyword: Higman's lemma keyword: extraction category: Mathematics/Combinatorics and Graph Theory category: Miscellaneous/Extracted Programs/Combinatorics
    Stefan Berghofer
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  38. coq-higman-nw

    No documentation

    A program from an A-translated impredicative proof of Higman's Lemma
    keyword: A-translation keyword: Higman's lemma keyword: impredicativity keyword: System F keyword: extraction category: Mathematics/Logic category: Mathematics/Combinatorics and Graph Theory category: Miscellaneous/Extracted Programs/Combinatorics
    Hugo Herbelin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  39. coq-higman-s

    No documentation

    Higman's lemma on an unrestricted alphabet
    keyword: Higman's lemma keyword: well quasi-ordering category: Mathematics/Combinatorics and Graph Theory date: 2007-09-14
    William Delobel <william.delobel@lif.univ-mrs.fr>
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  40. coq-historical-examples

    No documentation

    Historical examples developed in the (pure) Calculus of Constructions
    keyword: Newman's lemma keyword: Tarski's fixpoint theorem keyword: line formatting keyword: binary-search paradigm keyword: square root approximation keyword: Calculus of Constructions keyword: history of Coq category: Miscellaneous/Coq Use Examples
    Gérard Huet Christine Paulin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  41. coq-hoare-tut

    No documentation

    A Tutorial on Reflecting in Coq the generation of Hoare proof obligations
    category:Mathematics/Logic category:Computer Science/Semantics and Compilation/Semantics keyword:Hoare logic keyword:imperative program keyword:weakest precondition keyword:reflection logpath:HoareTut
    Sylvain Boulmé
    8.11.1
    LGPL-3.0-or-later
    Used by 0 other packages
    05 Jun 2020
  42. coq-hol-light

    No documentation

    HOL-Light library in Coq
    logpath:HOLLight date:2025-01-20 category:Mathematics/Arithmetic and Number Theory/Miscellaneous category:Mathematics/Real Numbers category:Mathematics/Real Calculus and Topology keyword:HOL-Light keyword:list keyword:basic set theory keyword:arithmetic keyword:integer keyword:real keyword:complex keyword:permutation keyword:group keyword:matroid keyword:binomial keyword:topology keyword:metric keyword:space keyword:analysis keyword:homology keyword:vector keyword:linear keyword:algebra keyword:convex keyword:path keyword:polytope keyword:Brouwer keyword:degree keyword:derivative keyword:Clifford keyword:integration keyword:measure keyword:Lebesgue keyword:transcendental
    Frédéric Blanqui
    3.0.0
    CeCILL-2.1
    Used by 0 other packages
    21 Jan 2025
  43. coq-hol-light-real-with-N

    No documentation

    Definition of HOL-Light real numbers in Coq using N
    logpath: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/coq-hol-light-real-with-N/blob/main/AUTHORS.md
    2.0.0
    CeCILL-2.1
    Used by 1 other packages
    11 Jul 2025
  44. coq-hol-light-real-with-nat

    No documentation

    Definition of HOL-Light real numbers in Coq using nat
    keyword:HOL-Light category:Math/Arith/Misc category:Math/Arith/Real numbers date:2024-11-03 logpath:HOLLight_Real
    Frédéric Blanqui
    1.0.0
    CeCILL-2.1
    Used by 1 other packages
    20 Jan 2025
  45. coq-hott

    No documentation

    The Homotopy Type Theory library
    logpath:HoTT
    The HoTT Library Development Team
    9.0
    BSD-2-Clause
    Used by 1 other packages
    29 Sep 2025
  46. coq-htt

    No documentation

    Hoare Type Theory
    category:Computer Science/Data Types and Data Structures keyword:partial commutative monoids keyword:separation logic logpath:htt
    Aleksandar Nanevski Germán Andrés Delbianco Alexander Gryzlov Marcos Grandury
    2.2.1
    Apache-2.0
    Used by 1 other packages
    16 Jun 2025
  47. coq-htt-core

    No documentation

    Hoare Type Theory
    category:Computer Science/Data Types and Data Structures keyword:partial commutative monoids keyword:separation logic logpath:htt
    Aleksandar Nanevski Germán Andrés Delbianco Alexander Gryzlov Marcos Grandury
    2.2.1
    Apache-2.0
    Used by 1 other packages
    16 Jun 2025
  48. coq-http

    No documentation

    HTTP in Coq
    category:Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols category:Miscellaneous/Extracted Programs/Decision procedures keyword:co-induction keyword:extraction keyword:reactive systems logpath:HTTP
    Yishuai Li <yishuai@cis.upenn.edu> Li-yao Xia <xialiyao@cis.upenn.edu> Yao Li <liyao@cis.upenn.edu> Azzam Althagafi <aazzam@cis.upenn.edu> Benjamin C. Pierce <bcpierce@cis.upenn.edu>
    0.2.1
    MPL-2.0
    Used by 0 other packages
    20 Jul 2023
  49. coq-huffman

    No documentation

    Coq proof of the correctness of the Huffman coding algorithm
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Miscellaneous/Extracted Programs/Combinatorics keyword:data compression keyword:code keyword:huffman tree logpath:Huffman date:2023-07-09
    Laurent Théry
    8.16.0
    LGPL-2.1-or-later
    Used by 0 other packages
    01 Aug 2023
  50. coq-hydra-battles

    No documentation

    Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq
    category:Mathematics/Combinatorics and Graph Theory category:Mathematics/Logic/Foundations keyword:Ketonen-Solovay machinery keyword:ordinal numbers keyword:primitive recursive functions logpath:hydras date:2022-05-20
    Pierre Castéran Évelyne Contejean Jeremy Damour Russell O'Connor Karl Palmskog et al.
    0.9
    MIT
    Used by 2 other packages
    25 May 2022
... 3 4 5 ... 11