252 search results for "tag:"logpath:""

Showing 101 - 150
  1. 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
  2. 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. coq-idt

    No documentation

    Inductive Definition Transformers
    category:Miscellaneous/Coq Extensions date:2024-05-12 logpath:idt
    Qianchuan Ye Benjamin Delaware
    1.3.0
    MIT
    Used by 0 other packages
    13 May 2024
  4. coq-infotheo

    No documentation

    Discrete probabilities and information theory for Coq
    keyword:information theory keyword:probability keyword:error-correcting codes keyword:convexity logpath:infotheo date:2025-05-10
    Reynald Affeldt, AIST Manabu Hagiwara, Chiba U. (previously AIST) Jonas Senizergues, ENS Cachan (internship at AIST) Jacques Garrigue Kazuhiko Sakaguchi, Tsukuba U. et al.
    0.9.3
    LGPL-2.1-or-later
    Used by 1 other packages
    10 May 2025
  5. coq-interval

    No documentation

    A Coq tactic for proving bounds on real-valued expressions automatically
    keyword:interval arithmetic keyword:decision procedure keyword:floating-point arithmetic keyword:reflexive tactic keyword:Taylor models category:Mathematics/Real Calculus and Topology category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Interval date:2024-10-21
    Guillaume Melquiond <guillaume.melquiond@inria.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr> Pierre Roux <pierre.roux@onera.fr> Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>
    4.11.1
    CeCILL-C
    Used by 7 other packages
    22 Oct 2024
  6. coq-io

    No documentation

    A library for effects in Coq
    date:2019-07-23 logpath:Io keyword:effects
    Guillaume Claret
    4.0.0
    MIT
    Used by 5 other packages
    23 Jul 2019
  7. coq-io-exception

    No documentation

    Abstract your errors into exceptions
    date:2015-06-14 keyword:effects logpath:Io
    Guillaume Claret
    1.1.0
    MIT
    Used by 1 other packages
    13 May 2019
  8. coq-io-system

    No documentation

    System effects for Coq
    date:2019-07-28 keyword:effects keyword:extraction logpath:Io.System
    Guillaume Claret
    2.4.1
    MIT
    Used by 2 other packages
    29 Jul 2019
  9. coq-iris

    No documentation

    A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
    date:2024-10-31 logpath:iris.prelude logpath:iris.algebra logpath:iris.si_logic logpath:iris.bi logpath:iris.proofmode logpath:iris.base_logic logpath:iris.program_logic
    The Iris Team
    4.3.0
    BSD-3-Clause
    Used by 2 other packages
    31 Oct 2024
  10. coq-iris-heap-lang

    No documentation

    The canonical example language for Iris
    date:2024-10-31 logpath:iris.heap_lang
    The Iris Team
    4.3.0
    BSD-3-Clause
    Used by 0 other packages
    31 Oct 2024
  11. coq-iris-string-ident

    No documentation

    Add support for Gallina names in intro patterns to the Iris Proof Mode
    category:Miscellaneous/Coq Extensions keyword:iris logpath:iris_string_ident
    Tej Chajed <tchajed@mit.edu>
    0.1.0
    BSD-3-Clause
    Used by 0 other packages
    23 Jul 2020
  12. coq-itauto

    No documentation

    Reflexive SAT solver with Nelson-Oppen support, parameterised by a leaf tactic inside Coq
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:integers keyword:SAT keyword:SMT keyword:Nelson-Oppen keyword:automation logpath:Cdcl date:2024-06-17
    Frédéric Besson
    8.20.0
    MIT
    Used by 1 other packages
    06 Sep 2024
  13. coq-itree

    No documentation

    Library for representing recursive and impure programs with equational reasoning
    org:deepspec logpath:ITree date:2025-02-28
    Li-yao Xia Yannick Zakowski Paul He Chung-Kil Hur Gregory Malecha et al.
    5.2.1
    MIT
    Used by 5 other packages
    28 Feb 2025
  14. coq-itree-extra

    No documentation

    Extensions to coq-itree
    org:deepspec logpath: ITree.Extra date:2024-04-02
    Lucas Silver Irene Yoon Paul He Yannick Zakowski Steve Zdancewic
    5.2.0
    MIT
    Used by 0 other packages
    04 Apr 2024
  15. coq-itree-io

    No documentation

    Run interaction trees in IO
    logpath:ITreeIO
    Li-yao Xia <lysxia@gmail.com>
    0.1.1
    MIT
    Used by 2 other packages
    21 Jul 2023
  16. coq-jmlcoq

    No documentation

    Coq definition of the JML specification language and a verified runtime assertion checker for JML
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:JML keyword:Java Modeling Language keyword:runtime verification logpath:JML date:2022-06-26
    Hermann Lehner David Pichardie Andreas Kägi
    8.15.0
    MIT
    Used by 0 other packages
    10 Sep 2022
  17. coq-jsast

    No documentation

    A minimal JavaScript syntax tree carved out of the JsCert project
    keyword:javascript keyword:compiler date:2020-07-29 logpath:JsAst
    Martin Bodin <> Arthur Charguéraud <> Daniele Filaretti <> Philippa Gardner <> Sergio Maffeis <> et al.
    3.0.0
    BSD-2-Clause
    Used by 1 other packages
    26 May 2022
  18. coq-json

    No documentation

    JSON in Coq
    category:Computer Science/Data Types and Data Structures keyword:serialization keyword:JSON logpath:JSON
    Yishuai Li <liyishuai.lys@alibaba-inc.com>
    0.2.0
    BSD-3-Clause
    Used by 2 other packages
    09 Oct 2024
  19. coq-kami

    No documentation

    A work-in-progress language and compiler for verified low-level programming
    logpath:kami
    Massachusetts Institute of Technology Kevix SiFive
    0.0.3-rv32i
    MIT
    Used by 0 other packages
    03 Apr 2023
  20. coq-karp-miller

    No documentation

    Certified Karp-Miller algorithm for the covering of Petri nets
    category:Computer Science/Data Types and Data Structures date:2024-11-22 logpath:KarpMiller
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.1
    MPL-2.0
    Used by 0 other packages
    23 Nov 2024
  21. coq-katamaran

    No documentation

    Separation logic-based verification of instruction sets
    keyword:program verification keyword:separation logic keyword:symbolic execution keyword:instruction sets category:Computer Science/Semantics and Compilation/Semantics data:2022-07-19 logpath:Katamaran
    Dominique Devriese Georgy Lukyanov Sander Huyghebaert Steven Keuchel
    0.2.0
    BSD-2-Clause
    Used by 0 other packages
    21 Oct 2022
  22. coq-kruskal-almostfull

    No documentation

    Base Coq library for manipulating Almost Full relations
    category:Computer Science/Data Types and Data Structures date:2024-11-21 logpath:KruskalAfProp logpath:KruskalAfType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.2
    MPL-2.0
    Used by 5 other packages
    22 Nov 2024
  23. coq-kruskal-fan

    No documentation

    Extending Coq library for manipulating Almost Full relations with the FAN theorem
    category:Computer Science/Data Types and Data Structures date:2024-11-22 logpath:KruskalFanProp logpath:KruskalFanType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.2
    MPL-2.0
    Used by 3 other packages
    23 Nov 2024
  24. coq-kruskal-finite

    No documentation

    Coq library for manipulating finiteness, finite choice and decision as used in proof of Kruskal's tree theorem
    category:Computer Science/Data Types and Data Structures date:2024-11-21 logpath:KruskalFinite
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.5
    MPL-2.0
    Used by 5 other packages
    22 Nov 2024
  25. coq-kruskal-higman

    No documentation

    Extending Coq library for manipulating Almost Full relations with Higman's lemma
    category:Computer Science/Data Types and Data Structures date:2024-11-22 logpath:KruskalHigmanProp logpath:KruskalHigmanType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.3
    MPL-2.0
    Used by 2 other packages
    23 Nov 2024
  26. coq-kruskal-theorems

    No documentation

    Extending the Coq library for manipulating Almost Full relations with various forms of Kruskal's tree theorem
    category:Computer Science/Data Types and Data Structures date:2024-08-28 logpath:KruskalThmProp logpath:KruskalThmType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.2
    MPL-2.0
    Used by 1 other packages
    24 Nov 2024
  27. coq-kruskal-trees

    No documentation

    Coq library for manipulating rose trees (ie finitely branching) as used in proof of Kruskal's tree theorem
    category:Computer Science/Data Types and Data Structures date:2024-11-21 logpath:KruskalTrees
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.5
    MPL-2.0
    Used by 7 other packages
    22 Nov 2024
  28. coq-kruskal-veldman

    No documentation

    Wim Veldman's proof of Higman's and Kruskal tree theorems
    category:Computer Science/Data Types and Data Structures date:2024-11-24 logpath:KruskalVeldmanProp logpath:KruskalVeldmanType
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.3
    MPL-2.0
    Used by 1 other packages
    24 Nov 2024
  29. coq-lemma-overloading

    No documentation

    Libraries demonstrating design patterns for programming and proving with canonical structures in Coq
    category:Computer Science/Data Types and Data Structures keyword:canonical structures keyword:proof automation keyword:Hoare type theory keyword:lemma overloading logpath:LemmaOverloading date:2020-08-12
    Georges Gonthier Beta Ziliani Aleksandar Nanevski Derek Dreyer
    8.12.0
    GPL-3.0-or-later
    Used by 0 other packages
    13 Aug 2020
  30. coq-lens

    No documentation

    Generation of lenses for record datatypes
    logpath:Lens date: 2020-11-18
    Gregory Malecha <gregory@bedrocksystems.com>
    1.0.1+8.12
    LGPL2.1+BedRock
    Used by 0 other packages
    18 Nov 2020
  31. coq-libhyps

    No documentation

    Hypotheses manipulation library
    keyword:proof environment manipulation keyword:forward reasoning keyword:hypothesis naming category:Miscellaneous/Coq Extensions logpath:LibHyps date:2024-12-19
    Pierre Courtieu
    3.0.1
    MIT
    Used by 1 other packages
    19 Dec 2024
  32. coq-libvalidsdp

    No documentation

    LibValidSDP
    keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:Miscellaneous/Coq Extensions logpath:libValidSDP
    Pierre Roux <pierre.roux@onera.fr> Érik Martin-Dorel <erik.martin-dorel@irit.fr>
    1.0.4
    LGPL-2.1-or-later
    Used by 1 other packages
    07 Feb 2025
  33. coq-linearscan

    No documentation

    A linear scan register allocator in Coq
    keyword: register allocator category:Computer Science/Semantics and Compilation/Compilation date: 2022-07-23 logpath: Linearscan
    John Wiegley
    1.1.0
    BSD-3-Clause
    Used by 0 other packages
    23 Jul 2022
  34. coq-math-classes

    No documentation

    A library of abstract interfaces for mathematical structures in Coq
    logpath:MathClasses date:2024-04-23
    Eelis van der Weegen Bas Spitters Robbert Krebbers
    8.19.0
    MIT
    Used by 1 other packages
    23 Apr 2024
  35. coq-mathcomp-abel

    No documentation

    Abel - Ruffini's theorem
    keyword:algebra keyword:Galois keyword:Abel Ruffini keyword:unsolvability of quintincs logpath:Abel date:2022-07-13
    Sophie Bernard Cyril Cohen Assia Mahboubi Pierre-Yves Strub
    1.2.1
    CECILL-B
    Used by 0 other packages
    24 Oct 2022
  36. coq-mathcomp-algebra-tactics

    No documentation

    Ring, field, lra, nra, and psatz tactics for Mathematical Components
    logpath:mathcomp.algebra_tactics
    Kazuhiko Sakaguchi Pierre Roux
    1.2.5
    CECILL-B
    Used by 2 other packages
    09 May 2025
  37. coq-mathcomp-analysis

    No documentation

    An analysis library for mathematical components
    category:Mathematics/Real Calculus and Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:Landau notation keyword:logarithm keyword:sin keyword:cos keyword:tangent keyword:trigonometric function keyword:exponential keyword:differentiation keyword:derivative keyword:measure theory keyword:integration keyword:Lebesgue keyword:probability logpath:mathcomp.analysis
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.11.0
    CECILL-C
    Used by 7 other packages
    02 May 2025
  38. coq-mathcomp-analysis-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.11.0
    CECILL-C
    Used by 0 other packages
    02 May 2025
  39. coq-mathcomp-apery

    No documentation

    A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:apery recurrence keyword:irrationality keyword:creative telescoping logpath:mathcomp.apery date:2022-05-05
    Frédéric Chyzak Assia Mahboubi Thomas Sibut-Pinote
    1.0.2
    CECILL-C
    Used by 0 other packages
    05 May 2022
  40. coq-mathcomp-bigenough

    No documentation

    A small library to do epsilon - N reasoning
    keyword:bigenough keyword:asymptotic reasonning keyword:small scale reflection keyword:mathematical components logpath:mathcomp.bigenough
    Cyril Cohen
    1.0.2
    CeCILL-B
    Used by 8 other packages
    25 Jan 2025
  41. coq-mathcomp-cad

    No documentation

    Formal Proof of Cylindrical Algebraic Decomposition
    keyword:CAD logpath:SemiAlgebraic
    Cyril Cohen Boris Djalal Quentin Vermande
    1.1
    LGPL-3.0-or-later
    Used by 0 other packages
    12 Dec 2024
  42. coq-mathcomp-classical

    No documentation

    A library for classical logic for mathematical components
    category:Mathematics/Logic/Classical logic keyword:classical logic keyword:logic keyword:sets keyword:set theory keyword:function keyword:cardinal keyword:filter logpath:mathcomp.classical
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.11.0
    CECILL-C
    Used by 2 other packages
    02 May 2025
  43. coq-mathcomp-dioid

    No documentation

    Dioid
    keyword:dioid keyword:semiring keyword:complete dioid category:Miscellaneous/Coq Extensions logpath:mathcomp.dioid
    Lucien Rakotomalala <lucien.rakotomalala@onera.fr> Pierre Roux <pierre.roux@onera.fr>
    0.2
    CECILL-B
    Used by 0 other packages
    20 Dec 2021
  44. coq-mathcomp-experimental-reals

    No documentation

    A library for alternative real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.experimental_reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.11.0
    CECILL-C
    Used by 1 other packages
    02 May 2025
  45. coq-mathcomp-finmap

    No documentation

    Compatibility package for rocq-mathcomp-finmap
    keyword:finmap keyword:finset keyword:multiset logpath:mathcomp.finmap
    Cyril Cohen Kazuhiko Sakaguchi
    2.2.1
    CECILL-B
    Used by 6 other packages
    29 Apr 2025
  46. coq-mathcomp-multinomials

    No documentation

    A Multivariate polynomial Library for the Mathematical Components Library
    keyword:multinomials keyword:monoid algebra category:Mathematics/Algebra/Multinomials category:Mathematics/Algebra/Monoid algebra logpath:mathcomp.multinomials
    Pierre-Yves Strub
    2.4.0
    CECILL-B
    Used by 3 other packages
    10 May 2025
  47. coq-mathcomp-real-closed

    No documentation

    Mathematical Components Library on real closed fields
    keyword:real closed field logpath:mathcomp.real_closed date:2024-12-09
    Cyril Cohen Assia Mahboubi
    2.0.3
    CECILL-B
    Used by 5 other packages
    10 May 2025
  48. coq-mathcomp-reals

    No documentation

    A library for real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals keyword:extended real numbers logpath:mathcomp.reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.11.0
    CECILL-C
    Used by 3 other packages
    02 May 2025
  49. coq-mathcomp-reals-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.11.0
    CECILL-C
    Used by 4 other packages
    02 May 2025
  50. coq-mathcomp-sum-of-two-square

    No documentation

    A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file :
    logpath:mathcomp.contrib.sum_of_two_square
    Laurent Thery
    1.0.1
    MIT
    Used by 0 other packages
    09 May 2018
2 3 4 ... 6