270 search results for "tag:"logpath:""

Showing 51 - 100
  1. coq-elpi

    No documentation

    Compatibility metapackage for Elpi extension language after the Rocq renaming
    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 7 other packages
    19 Sep 2025
  2. coq-ext-lib

    No documentation

    A library of Coq definitions, theorems, and tactics
    logpath:ExtLib
    Gregory Malecha
    0.13.0
    BSD-2-Clause
    Used by 14 other packages
    06 Dec 2024
  3. coq-extructures

    No documentation

    Finite sets, maps, and other data structures with extensional reasoning
    keyword:finite maps keyword:extensionality category:Computer Science/Data Types and Data Structures logpath:extructures
    Arthur Azevedo de Amorim
    0.5.0
    MIT
    Used by 1 other packages
    10 Dec 2024
  4. coq-fcsl-pcm

    No documentation

    Coq library of Partial Commutative Monoids
    category:Computer Science/Data Types and Data Structures keyword:partial commutative monoids keyword:separation logic keyword:concurrency logpath:pcm
    Aleksandar Nanevski Anton Trunov Alexander Gryzlov
    2.2.0
    Apache-2.0
    Used by 4 other packages
    12 Jun 2025
  5. coq-fiat-crypto

    No documentation

    Cryptographic Primitive Code Generation by Fiat
    logpath:Crypto
    Andres Erbsen <andreser@mit.edu> Google Inc. Jade Philipoom <jadep@mit.edu> <jade.philipoom@gmail.com> Massachusetts Institute of Technology Zoe Paraskevopoulou <zoe.paraskevopoulou@gmail.com>
    0.1.3
    MIT OR Apache-2.0 OR BSD-1-Clause
    Used by 0 other packages
    22 Apr 2024
  6. coq-file-sync

    No documentation

    File synchroniser specification in Coq
    logpath:FileSync
    Yishuai Li <liyishuai.lys@alibaba-inc.com>
    0.1.0
    MPL-2.0
    Used by 0 other packages
    14 Sep 2022
  7. 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
  8. coq-flocq

    No documentation

    A formalization of floating-point arithmetic for the Coq system
    keyword:floating-point arithmetic logpath:Flocq date:2025-01-26
    Sylvie Boldo <sylvie.boldo@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>
    4.2.1
    LGPL-3.0-or-later
    Used by 18 other packages
    26 Jan 2025
  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-formalv-check_range

    No documentation

    Tactics to automatically prove Boolean goals involving Uint63/Sint63 variables
    keyword:automation keyword:primitive integers logpath:formalv.check_range
    Ana de Almeida Borges Quim Casals Buñuel Juan Conejero Rodriguez Mireia González Bedmar Eduardo Hermo Reyes
    1.4.0
    PolyForm Noncommercial License 1.0.0
    Used by 1 other packages
    29 Oct 2025
  11. coq-formalv-prim63_mathcomp

    No documentation

    Refinements from MathComp nat and int to Coq primitive integers Uint63/Sint63
    keyword:refinement keyword:primitive integers logpath:formalv.prim63_mathcomp
    Ana de Almeida Borges Quim Casals Buñuel Juan Conejero Rodriguez Mireia González Bedmar Eduardo Hermo Reyes
    1.4.0
    PolyForm Noncommercial License 1.0.0
    Used by 2 other packages
    29 Oct 2025
  12. coq-formalv-time

    No documentation

    A Coq library for time and date arithmetic according to the UTC standard with leap seconds
    keyword:time keyword:date keyword:timestamp logpath:formalv.time
    Ana de Almeida Borges Quim Casals Buñuel Juan Conejero Rodriguez Mireia González Bedmar Eduardo Hermo Reyes
    1.4.0
    PolyForm Noncommercial License 1.0.0
    Used by 0 other packages
    29 Oct 2025
  13. 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.1
    CECILL-B
    Used by 1 other packages
    21 Apr 2025
  14. 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:2025-04-16
    Georges Gonthier
    1.4.1
    CECILL-B
    Used by 4 other packages
    21 Apr 2025
  15. coq-fpmods

    No documentation

    A short constructive formalization of finitely presented modules
    logpath:fpmods
    Cyril Cohen and Anders Mörtberg
    0.2.0
    MIT
    Used by 0 other packages
    25 Nov 2015
  16. coq-freesim

    No documentation

    Stuttering For Free
    keyword:simulation keyword:coinduction keyword:dual non-determinism keyword:up to techniques keyword:companion keyword:Interaction Trees keyword:CompCert logpath:FreeSim
    Minki Cho, Youngju Song, Dongjae Lee
    1.0.0
    BSD-3-Clause
    Used by 0 other packages
    19 Sep 2023
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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
  50. 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
1 2 3 ... 6