33 search results for "tag:"category:Computer Science/Data Types and Data Structures""
-
coq-alea
No documentation
Coq library for reasoning on romized algorithms8.12.0LGPL-2.1-onlyUsed by 0 other packages03 Nov 2021 -
coq-almost-full
No documentation
Almost-full relations in Coq for proving termination8.18.0MITUsed by 0 other packages28 Dec 2023 -
coq-bits
No documentation
A bit vector library1.1.0Apache-2.0Used by 0 other packages12 Jul 2021 -
coq-ceramist
No documentation
Coq library for reasoning about probabilistic algorithms1.0.1GPL-3.0-or-laterUsed by 0 other packages06 Apr 2020 -
coq-color
No documentation
A library on rewriting theory terminationdate:2024-04-16 logpath:CoLoR category:Computer Science/Decision Procedures Certified Algorithms/Correctness proofs of algorithms category:Computer Structures category:Computer Science/Lambda Calculi category:Mathematics/Algebra category:Mathematics/Combinatorics Graph Theory category:Mathematics/Logic/Type theory category:Miscellaneous/Extracted Programs/Type checking unification normalization keyword:rewriting keyword:termination keyword:lambda calculus keyword:list keyword:multiset keyword:polynomial keyword:vectors keyword:matrices keyword:FSet keyword:FMap keyword:term keyword:context keyword:substitution keyword:universal algebra keyword:varyadic term keyword:string keyword:alpha-equivalence keyword:de Bruijn indices keyword:simple keyword:matching keyword:unification keyword:relation keyword:ordering keyword:quasi-ordering keyword:lexicographic ordering keyword:ring keyword:semiring keyword:well-foundedness keyword:noetherian keyword:finitely branching keyword:dependent choice keyword:infinite sequences keyword:non-termination keyword:loop keyword:graph keyword:path keyword:transitive closure keyword:strongly connected components keyword:topological ordering keyword:rpo keyword:horpo keyword:dependency pair keyword:dependency graph keyword:semantic labeling keyword:reducibility keyword:Girard keyword:fixpoint theorem keyword:Tarski keyword:pigeon-hole principle keyword:Ramsey theorem1.8.5CeCILL-2.1Used by 0 other packages16 Apr 2024 -
coq-deriving
No documentation
Generic instances of MathComp classes0.2.2MITUsed by 2 other packages18 Apr 2025 -
coq-diqt
No documentation
Formalization of hashtables with Radix trees PArray1.0.0CECILL-BUsed by 0 other packages13 Jul 2023 -
coq-extructures
No documentation
Finite sets, maps, other structures with extensional reasoning0.5.0MITUsed by 1 other packages10 Dec 2024 -
coq-fcsl-pcm
No documentation
Coq library of Partial Commutative Monoids2.2.0Apache-2.0Used by 4 other packages12 Jun 2025 -
coq-friedman-tree
No documentation
Implementation of Friedman's TREE function based on Kruskal's theorem1.1MPL-2.0Used by 0 other packages23 May 2024 -
coq-htt
No documentation
Hoare Type Theory2.2.1Apache-2.0Used by 1 other packages16 Jun 2025 -
coq-htt-core
No documentation
Hoare Type Theory2.2.1Apache-2.0Used by 1 other packages16 Jun 2025 -
coq-json
No documentation
JSON in Coq0.2.0BSD-3-ClauseUsed by 2 other packages09 Oct 2024 -
coq-karp-miller
No documentation
Certified Karp-Miller algorithm for the covering of Petri nets1.1MPL-2.0Used by 0 other packages23 Nov 2024 -
coq-kruskal-almostfull
No documentation
Base Coq library for manipulating Almost Full relations2.1MPL-2.0Used by 5 other packages06 Mar 2026 -
coq-kruskal-fan
No documentation
Extending Coq library for manipulating Almost Full relations with the FAN theorem2.1MPL-2.0Used by 3 other packages03 Mar 2026 -
coq-kruskal-finite
No documentation
Coq library for manipulating finiteness, finite choice decision as used in proof of Kruskal's tree theorem2.0MPL-2.0Used by 5 other packages24 Nov 2025 -
coq-kruskal-higman
No documentation
Extending Coq library for manipulating Almost Full relations with Higman's lemma2.0MPL-2.0Used by 2 other packages08 Jan 2026 -
coq-kruskal-theorems
No documentation
Extending the Coq library for manipulating Almost Full relations with various forms of Kruskal's tree theorem2.0MPL-2.0Used by 1 other packages08 Jan 2026 -
coq-kruskal-trees
No documentation
Coq library for manipulating rose trees (ie finitely branching) as used in proof of Kruskal's tree theorem2.0.1MPL-2.0Used by 7 other packages06 Mar 2026 -
coq-kruskal-veldman
No documentation
Wim Veldman's proof of Higman's Kruskal tree theorems2.1MPL-2.0Used by 1 other packages06 Mar 2026 -
coq-lemma-overloading
No documentation
Libraries demonstrating design patterns for programming proving with canonical structures in Coq8.12.0GPL-3.0-or-laterUsed by 0 other packages13 Aug 2020 -
coq-mathcomp-word
No documentation
Yet Another Coq Library on Machine Words3.4MITUsed by 1 other packages11 Mar 2026 -
coq-mmaps
No documentation
Several implementations of finite maps over arbitrary ordered using Coq functors1.1LGPL-2.1-onlyUsed by 0 other packages08 Jan 2024 -
coq-msets-extra
No documentation
Extensions of MSets for Efficient Execution1.2.0LGPL-2.1-onlyUsed by 0 other packages19 Sep 2019 -
coq-parsec
No documentation
Monadic parser combinator library in Coq0.2.0BSD-3-ClauseUsed by 2 other packages09 Oct 2024 -
coq-parseque
No documentation
Total parser combinators in Coq0.2.2MITUsed by 1 other packages10 Mar 2025 -
coq-record-update
No documentation
Generic support for updating record fields in Coq0.3.6MITUsed by 2 other packages08 Sep 2025 -
coq-tlc
No documentation
TLC: A Library for Classical Coq20260120MITUsed by 2 other packages20 Jan 2026 -
coq-void
No documentation
MathComp instances for the empty type (Empty_set)0.1.0MITUsed by 0 other packages08 Oct 2019 -
rocq-ceres-bytestring
No documentation
Library for serialization via S-expressions using bytestrings1.0.0MITUsed by 2 other packages11 Mar 2026 -
rocq-color
No documentation
A library on rewriting theory terminationdate:2025-11-11 logpath:CoLoR category:Computer Science/Algorithms/Correctness proofs of algorithms category:Computer Structures category:Computer Science/Lambda Calculi category:Mathematics/Algebra category:Mathematics/Combinatorics Graph Theory category:Mathematics/Logic/Type theory category:Miscellaneous/Extracted Programs/Type checking unification normalization keyword:rewriting keyword:termination keyword:lambda calculus keyword:list keyword:multiset keyword:polynom keyword:vectors keyword:matrices keyword:FSet keyword:FMap keyword:term keyword:context keyword:substitution keyword:universal algebra keyword:varyadic term keyword:string keyword:alpha-equivalence keyword:de bruijn indices keyword:simple keyword:matching keyword:unification keyword:relation keyword:ordering keyword:quasi-ordering keyword:lexicographic ordering keyword:ring keyword:semiring keyword:well-founded keyword:noetherian keyword:finitely branching keyword:dependent choice keyword:infinite sequences keyword:non-termination keyword:loop keyword:graph keyword:path keyword:transitive closure keyword:strongly connected component keyword:topological ordering keyword:rpo keyword:horpo keyword:dependency pair keyword:dependency graph keyword:semantic labeling keyword:reducibility keyword:Girard keyword:fixpoint theorem keyword:Tarski keyword:pigeon-hole principle keyword:Ramsey theorem1.8.6CeCILL-2.1Used by 0 other packages11 Nov 2025 -
rocq-parseque
No documentation
Total parser combinators in Rocq/Coq0.3.0MITUsed by 0 other packages27 Jun 2025