522 search results for ""

Showing 201 - 250
  1. 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
  2. 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
  3. 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
  4. 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
  5. coq-improper-integrals

    No documentation

    Additions to the coquelicot library for handling improper integrals
    keyword:real analysis category:Mathematics/Real Calculus and Topology
    Yves Bertot <yves.bertot@inria.fr>
    0.1.0
    MIT
    Used by 0 other packages
    19 Apr 2018
  6. 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
  7. 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
  8. 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
  9. 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
  10. coq-intuitionistic-nuprl

    No documentation

    An Impredicative Model of Nuprl's Constructive Type Theory
    keyword: Nuprl keyword: computational type theory keyword: extensional type theory keyword: intuitionistic type theory keyword: Howe's computational equivalence relation keyword: Partial Equivalence Relation (PER) semantics keyword: consistency keyword: continuity keyword: bar induction category: Mathematics/Logic/Type theory
    Vincent Rahli <vincent.rahli@gmail.com> [http://www.cs.cornell.edu/~rahli/] Abhishek Anand <abhishek.anand.iitg@gmail.com> [http://www.cs.cornell.edu/~aa755/] Mark Bickford <mark.concertina@gmail.com> [http://nuprl.org/]
    8.6.0
    GPL
    Used by 0 other packages
    20 Nov 2018
  11. 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
  12. 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
  13. 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
  14. 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
  15. coq-io-list

    No documentation

    Generic functions on lists with effects
    Guillaume Claret
    1.1.0
    MIT
    Used by 1 other packages
    25 Nov 2015
  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-ipc

    No documentation

    Intuitionistic Propositional Checker
    keyword: intuitionistic logic keyword: proof search keyword: proof-as-programs keyword: correct-by-construction keyword: program verification keyword: program extraction category: Mathematics/Logic/Foundations category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category: Miscellaneous/Extracted Programs/Decision procedures
    Klaus Weich
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  19. 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
  20. 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
  21. 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
  22. 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
  23. coq-iterable

    No documentation

    Generic definition of iterators
    Guillaume Claret
    1.0.0
    MIT
    Used by 1 other packages
    25 Nov 2015
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. coq-label

    No documentation

    'label' is a Coq plugin for referring to Propositional hypotheses by their type
    Pierre-Évariste Dagand Théo Zimmermann Pierre-Marie Pédrot
    1.0.0
    MIT
    Used by 0 other packages
    26 Mar 2018
  46. coq-lambda

    No documentation

    Residual Theory in Lambda-Calculus
    keyword: pure lambda-calculus keyword: confluence keyword: parallel-moves lemma keyword: Lévy's Cube Lemma keyword: Church-Rosser keyword: residual keyword: Prism theorem category: Computer Science/Lambda Calculi
    Gérard Huet
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  47. 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
  48. coq-lazy-pcf

    No documentation

    Subject Reduction for Lazy-PCF
    keyword: functional programming keyword: lazy evaluation keyword: operational semantics keyword: type soundness keyword: normal forms category: Computer Science/Lambda Calculi
    Amy Felty Jill Seaman
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  49. 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
  50. coq-lean-import

    No documentation

    Plugin allowing Coq to import Lean exported files
    logpath:LeanImport
    Gaëtan Gilbert
    9.0+lean3-alpha
    LGPL-2.1-only
    Used by 0 other packages
    28 Aug 2025
... 4 5 6 ... 11