282 search results for "tag:"date:""

Showing 51 - 100
  1. coq-dpdgraph

    No documentation

    Compute dependencies between Coq objects (definitions, theorems) and produce graphs
    category:Miscellaneous/Coq Extensions keyword:dependency graph keyword:dependency analysis logpath:dpdgraph date:2025-05-28
    Anne Pacalet Yves Bertot Olivier Pons
    1.0+9.1
    LGPL-2.1-only
    Used by 0 other packages
    10 Dec 2025
  2. coq-euler-formula

    No documentation

    Hypermaps, Genus Theorem and Euler Formula
    keyword: polyhedron keyword: hypermap keyword: genus keyword: Euler formula keyword: assisted proofs category: Mathematics/Geometry date: 2006-09
    Jean-François Dufourd <dufourd@dpt-info.u-strasbg.fr> [http://dpt-info.u-strasbg.fr/~jfd/]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  3. coq-fairisle

    No documentation

    Proof of the Fairisle 4x4 Switch Element
    keyword: circuits keyword: automata keyword: co-induction keyword: dependent types category: Computer Science/Architecture date: 2005-12-15
    Solange Coupet-Grimal <Solange.Coupet@lif.univ-mrs.fr> [http://www.cmi.univ-mrs.fr/~solange/] Line Jakubiec-Jamet <Line.Jakubiec@lif.univ-mrs.fr> [http://www.dil.univ-mrs.fr/~jakubiec/]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  4. coq-fermat4

    No documentation

    Diophantus' 20th Problem and Fermat's Last Theorem for n = 4
    keyword: Diophantus keyword: Fermat keyword: arithmetic keyword: infinite descent category: Mathematics/Arithmetic and Number Theory/Number theory date: 2005-07
    David Delahaye Micaela Mayero
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  5. coq-finger-tree

    No documentation

    Dependent Finger Trees
    keyword: data structures keyword: dependent types keyword: Finger Trees category: Computer Science/Data Types and Data Structures date: 2009-02
    Matthieu Sozeau <mattam@mattam.org> [http://mattam.org]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  6. coq-finmatrix

    No documentation

    Matrix by fin (finite set over nat) in Coq
    keyword:matrices category:Mathematics/Algebra date:2024-06-11 logpath:FinMatrix
    ZhengPu Shi
    1.0.2
    MIT
    Used by 0 other packages
    11 Jun 2024
  7. coq-float

    No documentation

    Library for floating-point numbers
    keyword: floating-point arithmetic category: Computer Science/Data Types and Data Structures date: 2001
    Laurent Théry Sylvie Boldo
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  8. coq-flocq

    No documentation

    A formalization of floating-point arithmetic for the Coq system
    keyword:floating-point arithmetic logpath:Flocq date:2026-02-19
    Sylvie Boldo <sylvie.boldo@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>
    4.2.2
    LGPL-3.0-or-later
    Used by 25 other packages
    19 Feb 2026
  9. coq-flocq-quickchick

    No documentation

    Flocq binary_float generators for QuickChick testing framework
    logpath: FlocqQuickChick date: 2020-04-01
    Yaroslav Kogevnikov <ykozhevnikov@codeminders.com>
    1.0.2
    MIT
    Used by 0 other packages
    03 Apr 2020
  10. coq-fourcolor

    No documentation

    Mechanization of the Four Color Theorem in Coq
    category:Mathematics/Combinatorics and Graph Theory keyword:Four color theorem keyword:small scale reflection keyword:Mathematical Components logpath:fourcolor.proof date:2025-04-16
    Georges Gonthier
    1.4.3
    CECILL-B
    Used by 1 other packages
    24 Jul 2026
  11. coq-fourcolor-reals

    No documentation

    Interface for real numbers used in the Four Color Theorem
    category:Mathematics/Real Calculus and Topology keyword:real numbers logpath:fourcolor.reals date:2026-07-17
    Georges Gonthier
    1.4.3
    CECILL-B
    Used by 4 other packages
    24 Jul 2026
  12. coq-freespec-core

    No documentation

    A framework for implementing and certifying impure computations in Coq
    date:2021-03-01 keyword:effects keyword:freer keyword:program logic category:Mathematics/Category Theory logpath:FreeSpec.Core
    Thomas Letan Yann Régis-Gianas
    0.3
    MPL-2.0
    Used by 2 other packages
    04 Mar 2021
  13. coq-freespec-exec

    No documentation

    A framework for implementing and certifying impure computations in Coq
    date:2021-03-01 keyword:plugin category:Miscellaneous/Coq Extensions logpath:FreeSpec.Exec
    Thomas Letan Yann Régis-Gianas
    0.3
    MPL-2.0
    Used by 0 other packages
    04 Mar 2021
  14. coq-freespec-ffi

    No documentation

    A framework for implementing and certifying impure computations in Coq
    date:2021-03-01 keyword:foreign function interface category:Miscellaneous/Coq Extensions logpath:FreeSpec.FFI
    Thomas Letan Yann Régis-Gianas
    0.3
    MPL-2.0
    Used by 1 other packages
    04 Mar 2021
  15. coq-friedman-tree

    No documentation

    Implementation of Friedman's TREE function based on Kruskal's theorem
    category:Computer Science/Data Types and Data Structures date:2024-05-23 logpath:FriedmanTREE
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.1
    MPL-2.0
    Used by 0 other packages
    23 May 2024
  16. coq-fssec-model

    No documentation

    Formal verification of an extension of a UNIX compatible, secure filesystem
    keyword: security keyword: filesystem keyword: UNIX keyword: MLS keyword: access control category: Computer Science/Operating Systems date: 2002-04-24
    Maximiliano Cristiá
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  17. coq-functional-algebra

    No documentation

    This package provides a Coq formalization of abstract algebra using
    keyword:algebra keyword:abstract algebra category:Miscellaneous/Coq Extensions date:2018-08-11 logpath:functional-algebra
    Larry D. Lee Jr.
    1.0.2
    LGPL-3.0
    Used by 0 other packages
    24 Aug 2018
  18. coq-functions-in-zfc

    No documentation

    Functions in classical ZFC
    keyword: set theory keyword: Zermelo-Fraenkel keyword: functions category: Mathematics/Logic/Set theory date: April 2001
    Carlos Simpson <carlos@math.unice.fr>
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  19. coq-fundamental-arithmetics

    No documentation

    Fundamental theorems of arithmetic
    keyword: arithmetic keyword: number theory category: Mathematics/Arithmetic and Number Theory/Miscellaneous date: 2008-02-1
    Sébastien Briais <sebastien.briais at ens-lyon.fr> [http://perso.ens-lyon.fr/sebastien.briais/]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  20. coq-gaia

    No documentation

    Implementation of books from Bourbaki's Elements of Mathematics in Coq
    category:Mathematics/Logic/Set theory keyword:Bourbaki keyword:set theory logpath:gaia date:2021-10-28
    José Grimm Alban Quadrat Carlos Simpson
    1.13
    MIT
    Used by 1 other packages
    30 Oct 2021
  21. coq-gaia-hydras

    No documentation

    Bridge in Coq between Gaia and Hydra battles
    category:Mathematics/Logic/Foundations keyword:ordinal numbers logpath:gaia_hydras date:2022-05-20
    Pierre Castéran
    0.9
    MIT
    Used by 0 other packages
    25 May 2022
  22. 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.4
    MIT
    Used by 0 other packages
    24 Jul 2026
  23. 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.4
    MIT
    Used by 1 other packages
    24 Jul 2026
  24. 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.4
    MIT
    Used by 1 other packages
    24 Jul 2026
  25. 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.4
    MIT
    Used by 0 other packages
    24 Jul 2026
  26. 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.4
    MIT
    Used by 2 other packages
    24 Jul 2026
  27. 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:2026-06-02
    Guillaume Melquiond <guillaume.melquiond@inria.fr>
    1.11.0
    LGPL-3.0-or-later
    Used by 0 other packages
    02 Jun 2026
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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.7
    CECILL-B
    Used by 0 other packages
    13 Nov 2025
  40. 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
  41. coq-hammer

    No documentation

    General-purpose automated reasoning hammer tool for Coq
    category:Miscellaneous/Coq Extensions keyword:automation keyword:hammer logpath:Hammer.Plugin date:2026-07-07
    Lukasz Czajka <lukaszcz@mimuw.edu.pl> Cezary Kaliszyk <cezary.kaliszyk@uibk.ac.at>
    1.3.3+9.2
    LGPL-2.1-only
    Used by 1 other packages
    09 Jul 2026
  42. coq-hammer-tactics

    No documentation

    Reconstruction tactics for the hammer for Coq
    keyword:automation keyword:hammer keyword:tactics logpath:Hammer.Tactics date:2026-07-07
    Lukasz Czajka <lukaszcz@mimuw.edu.pl>
    1.3.3+9.2
    LGPL-2.1-only
    Used by 2 other packages
    09 Jul 2026
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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
  50. 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
1 2 3 ... 6