254 search results for "tag:"date:""

Showing 101 - 150
  1. 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
  2. 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
  3. 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
  4. coq-icharate

    No documentation

    Icharate: A logical Toolkit for Multimodal Categorial Grammars
    keyword: multimodal categorial grammars keyword: syntax/semantics interface keyword: higher-order logic keyword: meta-linguistics category: Computer Science/Formal Languages Theory and Automata date: 2003-2006
    Houda Anoun <anoun@labri.fr> Pierre Casteran <casteran@labri.fr>
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  5. 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
  6. coq-idxassoc

    No documentation

    Associative Arrays
    keyword: associative arrays keyword: search operator keyword: data structures category: Computer Science/Data Types and Data Structures date: April 2001
    Dominique Quatravaux François-René Ridaux Gérald Macinenti
    8.10.0
    BSD with advertising clause
    Used by 0 other packages
    07 Dec 2019
  7. coq-ieee754

    No documentation

    A formalisation of the IEEE754 norm on floating-point arithmetic
    keyword: floating-point arithmetic keyword: IEEE category: Computer Science/Data Types and Data Structures category: Computer Science/Semantics and Compilation/Semantics date: 1997
    Patrick Loiseleur
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  8. coq-inconsequential_modus_ponens

    No documentation

    A Coq library about how redundant modus ponens is
    keyword:modus ponens category:Mathematics/Logic/Foundations date:2022-08-20
    Veeti Eronen
    1.0.6
    CC-BY-SA-3.0
    Used by 0 other packages
    25 Sep 2022
  9. 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-09-16
    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.5
    LGPL-2.1-or-later
    Used by 1 other packages
    16 Sep 2025
  10. coq-int-map

    No documentation

    Maps indexed by binary integers : IntMap
    keyword: finite sets keyword: maps keyword: binary integers keyword: efficient data structures keyword: data structures category: Computer Science/Data Types and Data Structures date: around 1999 (integrated within Coq 7.0)
    Jean Goubault <goubault [@] lsv.ens-cachan.fr>
    8.10.0
    Unknown
    Used by 4 other packages
    07 Dec 2019
  11. 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:2025-07-31
    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.3
    CeCILL-C
    Used by 8 other packages
    31 Jul 2025
  12. 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
  13. coq-io-evaluate

    No documentation

    Generic functions to run effects
    date:2015-06-14 keyword:effects
    Guillaume Claret
    1.0.0
    MIT
    Used by 1 other packages
    14 May 2019
  14. 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
  15. coq-io-hello-world

    No documentation

    A Hello World program in Coq
    date:2019-07-30 keyword:effects keyword:extraction
    Guillaume Claret
    1.2.0
    MIT
    Used by 0 other packages
    30 Jul 2019
  16. 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
  17. coq-io-system-ocaml

    No documentation

    Extraction to OCaml of system effects
    date:2019-07-25 keyword:effects keyword:extraction
    Guillaume Claret
    2.3.1
    MIT
    Used by 2 other packages
    26 Jul 2019
  18. coq-iris

    No documentation

    A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
    date:2025-06-04 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.4.0
    BSD-3-Clause
    Used by 2 other packages
    12 Jun 2025
  19. coq-iris-heap-lang

    No documentation

    The canonical example language for Iris
    date:2025-06-04 logpath:iris.heap_lang
    The Iris Team
    4.4.0
    BSD-3-Clause
    Used by 0 other packages
    12 Jun 2025
  20. 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
  21. 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 6 other packages
    28 Feb 2025
  22. coq-itree-extra

    No documentation

    Extensions to coq-itree
    org:deepspec logpath:ITree date:2025-02-28
    Lucas Silver Irene Yoon Paul He Yannick Zakowski Steve Zdancewic
    5.2.1
    MIT
    Used by 0 other packages
    30 Jun 2025
  23. coq-izf

    No documentation

    Intuitionistic Zermelo-Fraenkel Set Theory in Coq
    keyword: Intuitionistic set theory keyword: pointed graphs keyword: type theory keyword: intuitionistic choice operator keyword: set theory keyword: Zermelo-Fraenkel category: Mathematics/Logic/Set theory date: 2003-02
    Alexandre Miquel <Alexandre.Miquel@pps.jussieu.fr> [http://www.pps.jussieu.fr/~miquel]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  24. 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
  25. coq-jordan-curve-theorem

    No documentation

    Hypermaps, planarity and discrete Jordan curve theorem
    keyword: combinatorial hypermaps keyword: genus keyword: planarity keyword: Euler formula keyword: Discrete Jordan Curve Theorem category: Mathematics/Geometry/General date: 2008
    Jean-François Dufourd <dufourd@lsiit.u-strasbg.fr> [http://dpt-info.u-strasbg.fr/~jfd/]
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  26. coq-jprover

    No documentation

    A theorem prover for first-order intuitionistic logic
    keyword: decision procedure keyword: first-order logic keyword: intuitionistic logic keyword: theorem proving keyword: proof search category: Miscellaneous/Coq Extensions category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures date: 2002-04 (contribution since January 2009)
    Huang Guan-Shieng
    8.6.0
    Unknown
    Used by 0 other packages
    20 Nov 2018
  27. 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
  28. coq-karatsuba

    No documentation

    Karatsuba's Multiplication
    keyword: Karatsuba multiplication keyword: binary ring category: Mathematics/Arithmetic and Number Theory/Number theory date: 2005-09-15
    Russell O'Connor <r.oconnor@cs.ru.nl> [http://r6.ca/]
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  29. 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
  30. coq-kildall

    No documentation

    Application of the Generic kildall's Data Flow Analysis Algorithm to a Type and Shape Static Analyses of Bytecode
    keyword: Kildall keyword: data flow analysis keyword: bytecode verification category: Computer Science/Semantics and Compilation/Semantics date: 2005-07
    Solange Coupet-Grimal <Solange.Coupet@cmi.univ-mrs.fr> William Delobel <delobel@cmi.univ-mrs.fr>
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. coq-lambek

    No documentation

    A Coq Toolkit for Lambek Calculus
    keyword: Computational linguistic keyword: categorial grammar keyword: Lambek calculus... category: Computer Science/Formal Languages Theory and Automata date: March-July 2003
    Houda Anoun <anoun@labri.fr> Pierre Castéran <casteran@labri.fr>
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  39. coq-lc

    No documentation

    Modules over monads and lambda-calculi
    keyword: modules keyword: monads keyword: category keyword: lambda calculus keyword: higher-order syntax category: Computer Science/Lambda Calculi date: 2006-01-12 date: 2008-09-9
    André Hirschowitz <ah@math.unice.fr> [http://math.unice.fr/~ah/] Marco Maggesi <maggesi@math.unifi.it> [http://www.math.unifi.it/~maggesi/]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  40. coq-legacy-ring

    No documentation

    The former implementation of the ring tactic
    date: 1998-5
    Patrick Loiseleur
    8.6.0
    Unknown
    Used by 0 other packages
    12 May 2019
  41. 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
  42. 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
  43. coq-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
    3.0.2
    MIT
    Used by 1 other packages
    14 Oct 2025
  44. coq-lin-alg

    No documentation

    Linear Algebra
    keyword: linear algebra category: Mathematics/Algebra date: 19 spetember 2003
    Jasper Stein <jasper@cs.kun.nl>
    8.9.0
    LGPL 2.1
    Used by 1 other packages
    08 Dec 2019
  45. 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
  46. coq-ltl

    No documentation

    Linear Temporal Logic
    keyword: temporal logic keyword: infinite transition systems keyword: co-induction category: Mathematics/Logic/Modal logic date: 2002-07
    Solange Coupet-Grimal
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  47. coq-maple-mode

    No documentation

    A Maple Mode for Coq
    keyword: Maple keyword: simplification keyword: field tactic category: Miscellaneous/Coq Extensions date: 2002-03
    David Delahaye Micaela Mayero
    8.9.0
    Unknown
    Used by 0 other packages
    08 Dec 2019
  48. coq-markov

    No documentation

    Markov's inequality
    keyword: probability keyword: Markov keyword: Lebesgue integration keyword: sigma algebras keyword: measurability keyword: Borel category: Mathematics/Real Calculus and Topology date: 2008-01-5
    Robert Kam <rkam2001@hotmail.com> [none]
    8.10.0
    GNU Lesser Public License
    Used by 0 other packages
    07 Dec 2019
  49. coq-math-classes

    No documentation

    A library of abstract interfaces for mathematical structures in Coq
    logpath:MathClasses date:2025-08-26
    Eelis van der Weegen Bas Spitters Robbert Krebbers
    9.0.0
    MIT
    Used by 1 other packages
    27 Aug 2025
  50. 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
2 3 4 ... 6