522 search results for ""

Showing 51 - 100
  1. coq-chick-blog

    No documentation

    A blog engine written and proven in Coq
    date:2019-11-26 keyword:blog keyword:effects keyword:extraction
    Guillaume Claret
    1.0.1
    MIT
    Used by 0 other packages
    01 Dec 2019
  2. coq-chinese

    No documentation

    A proof of the Chinese Remainder Lemma
    keyword: number theory keyword: chinese remainder keyword: primality keyword: prime numbers category: Mathematics/Arithmetic and Number Theory/Number theory
    Valérie Ménissier-Morain
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  3. coq-circuits

    No documentation

    Some proofs of hardware (adder, multiplier, memory block instruction)
    keyword: hardware verification category: Computer Science/Architecture
    Laurent Arditi
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  4. coq-classical-realizability

    No documentation

    Krivine's classical realizability
    keyword: classical realizability keyword: Krivine's realizability keyword: primitive datatype keyword: non determinism keyword: quote keyword: axiom of countable choice keyword: real numbers category: Mathematics/Logic/Foundations
    Lionel Rieg <lionel.rieg@ens-lyon.org>
    8.10.0
    BSD
    Used by 0 other packages
    19 Oct 2020
  5. coq-coalgebras

    No documentation

    Coalgebras, bisimulation and lambda-coiteration
    keyword: coalgebra keyword: bisimulation keyword: weakly final keyword: coiteration keyword: co-inductive types category: Mathematics/Category Theory date: 2008-10
    Milad Niqui <M.Niqui@cwi.nl> [http://www.cwi.nl/~milad]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  6. coq-coinduction

    No documentation

    Compatibility package for rocq-coinduction
    Damien Pous <Damien.Pous@ens-lyon.fr>
    1.21
    LGPL-3.0-or-later
    Used by 1 other packages
    19 Sep 2025
  7. coq-coinduction-examples

    No documentation

    Examples on how to use the coq-coinduction library, for doing proofs by (enhanced) coinduction
    keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity keyword:divergence keyword:streams keyword:CCS logpath:CoinductionExamples
    Damien Pous
    1.7
    LGPL-3.0-or-later
    Used by 0 other packages
    13 Jul 2023
  8. coq-coinductive-examples

    No documentation

    Some simple examples about co-inductive types and co-induction
    keyword: co-inductive types keyword: co-induction category: Miscellaneous/Coq Use Examples
    Eduardo Giménez
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  9. coq-coinductive-reals

    No documentation

    Real numbers as coinductive ternary streams
    keyword: real numbers keyword: co-inductive types keyword: co-recursion keyword: exact arithmetic category: Mathematics/Real Numbers date: 2007-04-24
    Milad Niqui <milad@cs.ru.nl> [http://www.cs.ru.nl/~milad]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  10. coq-color

    No documentation

    A library on rewriting theory and termination
    date:2023-06-28 logpath:CoLoR category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Computer Science/Data Types and Data Structures category:Computer Science/Lambda Calculi category:Mathematics/Algebra category:Mathematics/Combinatorics and Graph Theory category:Mathematics/Logic/Type theory category:Miscellaneous/Extracted Programs/Type checking unification and 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 types 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 theorem
    Frédéric Blanqui Adam Koprowski Sébastien Hinderer Pierre-Yves Strub Sidi Ould Biha et al.
    1.8.5
    CeCILL-2.1
    Used by 0 other packages
    16 Apr 2024
  11. coq-commutative-diagrams

    No documentation

    A Coq plugin to deal with commutative diagrams
    Luc Chabassier
    0.1
    MIT
    Used by 0 other packages
    18 Jul 2022
  12. coq-comp-dec-modal

    No documentation

    Constructive proofs of soundness and completeness for K, K*, CTL, PDL, and PDL with converse
    category:Mathematics/Logic/Modal logic keyword:modal logic keyword:completeness keyword:decidability keyword:Hilbert system keyword:computation tree logic keyword:propositional dynamic logic logpath:CompDecModal date:2024-07-24
    Christian Doczkal
    1.2
    CECILL-B
    Used by 0 other packages
    24 Jul 2024
  13. coq-compcert

    No documentation

    The CompCert C compiler (64 bit)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert date:2025-09-01
    Xavier Leroy
    3.16
    INRIA Non-Commercial License Agreement
    Used by 4 other packages
    08 Sep 2025
  14. coq-compcert-32

    No documentation

    The CompCert C compiler (32 bit)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert32 date:2023-07-04
    Xavier Leroy
    3.13.1
    INRIA Non-Commercial License Agreement
    Used by 1 other packages
    09 Nov 2023
  15. coq-compcert-64

    No documentation

    The CompCert C compiler (64 bit, using coq-platform supplied version of Flocq)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert64 date:2020-04-29
    Xavier Leroy
    3.7+8.12~coq_platform
    INRIA Non-Commercial License Agreement
    Used by 1 other packages
    28 Jul 2020
  16. coq-concat

    No documentation

    Constructive Category Theory
    keyword: category theory category: Mathematics/Category Theory
    Amokrane Saïbi
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  17. coq-concurrency-pluto

    No documentation

    A web server written in Coq
    Guillaume Claret
    1.1.0
    MIT
    Used by 0 other packages
    14 May 2019
  18. coq-concurrency-proxy

    No documentation

    A proxy to interface concurrent Coq programs with the operating system
    date:2015-01-28 keyword:effects keyword:extraction
    Guillaume Claret
    1.0.0
    MIT
    Used by 1 other packages
    14 May 2019
  19. coq-concurrency-system

    No documentation

    Experimental library to write concurrent applications in Coq
    date:2015-11-26 keyword:effects keyword:extraction
    Guillaume Claret
    1.1.0
    MIT
    Used by 1 other packages
    14 May 2019
  20. coq-constructive-geometry

    No documentation

    Elements of Constructive Geometry
    keyword: constructive mathematics keyword: geometry category: Mathematics/Geometry/General
    Gilles Kahn
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  21. coq-constructors

    No documentation

    An example Coq plugin, defining a tactic to get the constructors of an inductive type in a list
    Matthieu Sozeau <mattam@mattam.org>
    1.0.0
    MIT
    Used by 0 other packages
    25 Nov 2015
  22. coq-containers

    No documentation

    Containers: a typeclass-based library of finite sets/maps
    keyword: data structures keyword: type classes category: Computer Science/Data Types and Data Structures
    Stéphane Lescuyer
    8.10.0
    Unknown
    Used by 0 other packages
    19 Oct 2020
  23. coq-continuations

    No documentation

    A toolkit to reason with programs raising exceptions
    keyword: exceptions keyword: monads keyword: continuations keyword: cps category: Computer Science/Semantics and Compilation/Semantics category: Miscellaneous/Extracted Programs/Combinatorics
    Jean-François Monin
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  24. coq-coq-in-coq

    No documentation

    A formalisation of the Calculus of Construction
    keyword: calculus of constructions category: Mathematics/Logic/Type theory category: Miscellaneous/Extracted Programs/Type checking unification and normalization
    Bruno Barras
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  25. coq-coq2html

    No documentation

    Generates HTML documentation from Coq source files. Alternative to coqdoc
    Xavier Leroy
    1.4
    GPL-2.0-or-later
    Used by 0 other packages
    15 Jul 2024
  26. coq-coqeal

    No documentation

    CoqEAL - The Coq Effective Algebra Library
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:effective algebra keyword:elementary divisor rings keyword:Smith normal form keyword:mathematical components keyword:Bareiss keyword:Karatsuba multiplication keyword:refinements logpath:CoqEAL
    Guillaume Cano Cyril Cohen Maxime Dénès Érik Martin-Dorel Anders Mörtberg et al.
    2.1.0
    MIT
    Used by 3 other packages
    18 Feb 2025
  27. coq-coqeal-refinements

    No documentation

    A refinement framework (for algebra)
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:Karatsuba multiplication keyword:refinements logpath:CoqEAL_refinements
    Guillaume Cano Cyril Cohen Maxime Dénès Anders Mörtberg Vincent Siles
    0.9.1
    MIT
    Used by 0 other packages
    25 Nov 2015
  28. coq-coqeal-theory

    No documentation

    The theory needed by the CoqEAL refinement framework library
    category:Mathematics/Algebra keyword:effective algebra keyword:elementary divisor rings keyword:Smith normal form keyword:mathematical components keyword:Bareiss logpath:CoqEAL_theory
    Guillaume Cano Cyril Cohen Maxime Dénès Anders Mörtberg Vincent Siles
    0.9.1
    MIT
    Used by 2 other packages
    25 Nov 2015
  29. coq-coqffi

    No documentation

    Tool for generating Coq FFI bindings to OCaml libraries
    category:Miscellaneous/Coq Extensions keyword:foreign function interface keyword:extraction keyword:OCaml logpath:CoqFFI
    Thomas Letan Li-yao Xia Yann Régis-Gianas Yannick Zakowski
    1.0.0~beta8
    MIT
    Used by 0 other packages
    29 Apr 2023
  30. coq-coqoban

    No documentation

    Coqoban (Sokoban in Coq)
    category:Miscellaneous/Logical Puzzles and Entertainment keyword:Sokoban keyword:puzzles logpath:Coqoban
    Jasper Stein Hugo Herbelin
    8.13.0
    LGPL-2.1-or-later
    Used by 0 other packages
    21 Aug 2021
  31. coq-coqprime

    No documentation

    Certifying prime numbers in Coq
    Laurent Théry
    1.6.0
    LGPL-2.1-only
    Used by 1 other packages
    19 Dec 2024
  32. coq-coqprime-generator

    No documentation

    Certificate generator for prime numbers in Coq
    Laurent Théry
    1.1.2
    LGPL-2.1-only
    Used by 0 other packages
    16 Jan 2025
  33. coq-coqrel

    No documentation

    Binary logical relations library for the Coq proof assistant
    keyword:relations category:Mathematics/Logic/Type theory
    Jérémie Koenig
    0.1.0
    MIT
    Used by 0 other packages
    27 Jan 2017
  34. coq-coqtail

    No documentation

    Library of mathematical theorems and tools proved inside the Coq
    category:Mathematics/Real Calculus and Topology keyword:real analysis keyword:complex analysis date:2024-07-13 logpath:Coqtail
    Guillaume Allais Sylvain Dailler Hugo Férée Jean-Marie Madiot Pierre-Marie Pédrot et al.
    8.20
    LGPL-3.0-only
    Used by 0 other packages
    14 Jul 2024
  35. coq-coquelicot

    No documentation

    A Coq formalization of real analysis compatible with the standard library
    keyword:real analysis keyword:topology keyword:filters keyword:metric spaces category:Mathematics/Real Calculus and Topology logpath:Coquelicot date:2025-07-30
    Sylvie Boldo <sylvie.boldo@inria.fr> Catherine Lelay <catherine.lelay@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>
    3.4.4
    LGPL-3.0-or-later
    Used by 10 other packages
    30 Jul 2025
  36. coq-coqutil

    No documentation

    Coq library for tactics, basic definitions, sets, maps
    logpath:coqutil
    Massachusetts Institute of Technology
    0.0.7
    MIT
    Used by 2 other packages
    08 Oct 2025
  37. coq-corn

    No documentation

    The Coq Constructive Repository at Nijmegen
    category:Mathematics/Algebra category:Mathematics/Real Calculus and Topology category:Mathematics/Exact Real computation keyword:constructive mathematics keyword:algebra keyword:real calculus keyword:real numbers keyword:Fundamental Theorem of Algebra logpath:CoRN date:2025-08-28
    Evgeny Makarov Robbert Krebbers Eelis van der Weegen Bas Spitters Jelle Herold et al.
    9.0.0
    GPL-2.0
    Used by 0 other packages
    29 Aug 2025
  38. coq-counting

    No documentation

    Counting: a Coq plugin for measuring definitions/proofs
    keyword: statistics category: Miscellaneous/Coq Extensions
    Stéphane Lescuyer
    8.6.0
    Unknown
    Used by 1 other packages
    20 Nov 2018
  39. coq-cours-de-coq

    No documentation

    Various examples of Coq proofs
    category: Miscellaneous/Coq Use Examples
    Frédéric Prost Gilles Kahn
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  40. coq-ctltctl

    No documentation

    Computation Tree Logic for Reactive Systems and Timed Computation Tree Logic for Real Time Systems
    keyword: CTL keyword: TCTL keyword: real time keyword: reactive systems keyword: temporal logic keyword: timed automatas keyword: timed graphs keyword: discrete time keyword: modal logic category: Mathematics/Logic/Modal logic date: February-March 2000
    Carlos Daniel Luna
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  41. coq-ctree

    No documentation

    Library for representing recursive, non-deterministic and impure programs with equational reasoning
    category:CS/Semantics and Compilation/Semantics category:CS/Concurrency/Theory of concurrent systems keyword:simulation keyword:bisimilarity keyword:coinduction up-to keyword:process algebra keyword:cooperative multithreading logpath:CTree
    Nicolas Chappe Paul He Ludovic Henrio Yannick Zakowski Steve Zdancewic
    2.0
    MIT
    Used by 0 other packages
    29 Jul 2025
  42. coq-cunit

    No documentation

    Convenience functions for unit testing in Coq
    Guillaume Claret
    1.0.0
    MIT
    Used by 1 other packages
    25 Nov 2015
  43. coq-cybele

    No documentation

    A Coq plugin for simpler proofs by reflection or OCaml certificates
    Guillaume Claret
    1.3.0
    MIT
    Used by 0 other packages
    25 Nov 2015
  44. coq-dblib

    No documentation

    Dblib
    keyword: abstract syntax keyword: binders keyword: de Bruijn indices keyword: shift keyword: lift keyword: substitution category: Computer Science/Lambda Calculi
    Francois Pottier <francois.pottier@inria.fr> [http://gallium.inria.fr/~fpottier/]
    8.8.0
    GPL
    Used by 0 other packages
    06 Feb 2019
  45. coq-demos

    No documentation

    Demos of some Coq tools appeared in version V6.0
    keyword: sorting keyword: Cases keyword: Tauto keyword: AutoRewrite keyword: Prolog category: Miscellaneous/Coq Use Examples
    Coq group
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  46. coq-dep-map

    No documentation

    Dependent Maps
    keyword: maps keyword: dependent maps category: Computer Science/Data Types and Data Structures
    Lionel Rieg <lionel.rieg@college-de-france.fr>
    8.10.0
    CeCILL-B
    Used by 0 other packages
    07 Dec 2019
  47. coq-deriving

    No documentation

    Generic instances of MathComp classes
    keyword:generic programming category:Computer Science/Data Types and Data Structures logpath:deriving
    Arthur Azevedo de Amorim
    0.2.2
    MIT
    Used by 2 other packages
    18 Apr 2025
  48. coq-descente-infinie

    No documentation

    The Descente Infinie Tactic
    keyword: induction keyword: infinite descent category: Miscellaneous/Coq Extensions date: 2010-02
    Razvan Voicu <razvan@comp.nus.edu.sg> [http://www.comp.nus.edu.sg/~razvan/] Li Mengran <limengra@comp.nus.edu.sg> [http://www.comp.nus.edu.sg/~limengra]
    8.10.0
    GPL
    Used by 0 other packages
    19 Oct 2020
  49. coq-dictionaries

    No documentation

    Dictionaries (with modules)
    keyword: modules keyword: functors keyword: search trees category: Computer Science/Data Types and Data Structures category: Miscellaneous/Extracted Programs/Data structures date: 2003-02-6
    Pierre Castéran <casteran@labri.fr>
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  50. coq-dijkstra

    No documentation

    A Verified Implementation of Dijkstra's Algorithm
    keyword:graph theory keyword:shortest path keyword:Dijkstra's algorithm category:Computer Science/Graph Theory date:2021-03-02 logpath:Dijkstra
    Masayuki Mizuno <mizuno@wantedly.com>
    0.1.0
    MIT
    Used by 0 other packages
    05 Mar 2021
1 2 3 ... 11