522 search results for ""

Showing 401 - 450
  1. coq-shuffle

    No documentation

    Gilbreath's card trick
    keyword: Gilbreath's card trick keyword: binary sequences category: Miscellaneous/Logical Puzzles and Entertainment
    Gérard Huet
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  2. coq-simple-io

    No documentation

    IO monad for Coq
    date:2025-02-28 logpath:SimpleIO keyword:extraction keyword:effects
    Li-yao Xia Yishuai Li
    1.11.0
    MIT
    Used by 7 other packages
    28 Feb 2025
  3. coq-smc

    No documentation

    BDD based symbolic model checker for the modal mu-calculus
    keyword: BDD keyword: binary decision diagrams keyword: classical logic keyword: propositional logic keyword: garbage collection keyword: modal mu-calculus keyword: model checking keyword: symbolic model checking keyword: reflection category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures date: 2002-11
    Kumar Neeraj Verma <verma@lsv.ens-cachan.fr>
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  4. coq-smlms

    No documentation

    A formal semantics capturing value binding in a language with a powerful module system such as OCaml.
    category:Computer Science/Semantics and Compilation/Semantics keywords: adequacy keywords: modules keywords: module types keywords: OCaml keywords: refactoring keywords: renaming keywords: semantics logpath:AbstractRenaming date:2023-02-14
    Hugo Férée
    1.0.0
    MIT
    Used by 0 other packages
    16 Feb 2023
  5. coq-smpl

    No documentation

    Smpl: An Extensible Tactic for Coq
    Sigurd Schneider <sigurd.schneider@cs.uni-saarland.de> Yannick Forster <forster@cs.uni-saarland.de> Fabian Kunze <fabian.kunze@cs.uni-saarland.de> Kenji Maillard <kenji.maillard@inria.fr>
    8.20
    MIT
    Used by 1 other packages
    20 Oct 2024
  6. coq-smt-check

    No documentation

    Invoke SMT solvers to check goals
    logpath:SMT
    Gregory Malecha
    2.0.0
    MIT
    Used by 0 other packages
    19 Mar 2016
  7. coq-smtcoq

    No documentation

    A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword: SMT keyword: SAT keyword: automation logpath:SMTCoq
    Michaël Armand Valentin Blot Amina Bousalem Boris Djalal Louise Dubois de Prisque et al.
    2.3+8.20
    CECILL-C
    Used by 1 other packages
    19 Sep 2024
  8. coq-sniper

    No documentation

    A Coq plugin for general proof automation
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword: SMT keyword: automation logpath:Sniper
    Valentin Blot <Valentin.Blot@inria.fr> Louise Dubois de Prisque <Louise.Dubois-de-Prisque@inria.fr> Chantal Keller <ckeller@lmf.cnrs.fr Pierre Vial <Pierre.Vial@inria.fr>
    1.1+8.16
    CECILL-C
    Used by 0 other packages
    16 Jun 2023
  9. coq-square-matrices

    No documentation

    From Fast Exponentiation to Square Matrices
    keyword: exponentiation keyword: vectors keyword: matrices keyword: polymorphic recursion keyword: nested datatypes category: Mathematics/Algebra
    Jean-Christophe Filliâtre
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  10. coq-squiggle-eq

    No documentation

    An abstract formalization of variable bindings (both named and de-bruijn),
    Abhishek Anand Vincent Rahli
    1.0.4
    MIT
    Used by 0 other packages
    27 Jul 2018
  11. coq-ssprove

    No documentation

    A Foundational Framework for Modular Cryptographic Proofs
    keyword:cryptography logpath:SSProve
    SSProve team
    0.2.4
    MIT
    Used by 0 other packages
    24 Apr 2025
  12. coq-ssreflect

    No documentation

    The Small Scale Reflection extension
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    1.5.0
    CeCILL-B
    Used by 3 other packages
    13 May 2019
  13. coq-stalmarck

    No documentation

    Verified implementation of Stålmarck's algorithm for proving tautologies in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:boolean formula keyword:tautology checker logpath:Stalmarck.Algorithm date:2024-06-30
    Pierre Letouzey Laurent Théry
    8.20.0
    LGPL-2.1-or-later
    Used by 1 other packages
    06 Sep 2024
  14. coq-stalmarck-tactic

    No documentation

    Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm
    category:Miscellaneous/Coq Extensions category:Miscellaneous/Extracted Programs/Decision procedures keyword:boolean formula keyword:tautology checker keyword:tactics logpath:Stalmarck.Tactic date:2024-06-30
    Pierre Letouzey Laurent Théry
    8.20.0
    LGPL-2.1-or-later
    Used by 0 other packages
    06 Sep 2024
  15. coq-stdpp

    No documentation

    An extended "Standard Library" for Coq
    date:2025-06-04 logpath:stdpp
    The std++ team
    1.12.0
    BSD-3-Clause
    Used by 4 other packages
    12 Jun 2025
  16. coq-stdpp-bitvector

    No documentation

    A library for bitvectors based on std++
    date:2025-06-04 logpath:stdpp.bitvector
    The std++ team
    1.12.0
    BSD-3-Clause
    Used by 1 other packages
    12 Jun 2025
  17. coq-streams

    No documentation

    Specification of Eratosthene Sieve
    keyword: Streams keyword: Eratosthene Sieve keyword: prime numbers keyword: number theory keyword: primality category: Mathematics/Arithmetic and Number Theory/Number theory
    François Leclerc, Christine Paulin-Mohring
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  18. coq-string

    No documentation

    Definition of strings in Coq
    keyword: string keyword: ascii character category: Miscellaneous/Coq Extensions date: 2002-03
    Laurent Théry
    8.6.0
    LGPL 2.1
    Used by 0 other packages
    20 Nov 2018
  19. coq-subst

    No documentation

    The confluence of Hardin-Lévy lambda-sigma-lift-calcul
    keyword: lambda-sigma-lift-calculus keyword: explicit substitution keyword: Newman's lemma keyword: Yokouchi's lemma keyword: confluence keyword: rewriting category: Computer Science/Lambda Calculi
    Amokrane Saïbi
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  20. coq-sudoku

    No documentation

    Sudoku solver certified in Coq
    category:Miscellaneous/Logical Puzzles and Entertainment keyword:puzzles keyword:Davis-Putnam keyword:sudoku logpath:Sudoku date:2022-10-19
    Laurent Théry
    8.16.0
    LGPL-2.1-or-later
    Used by 0 other packages
    19 Oct 2022
  21. coq-sum-of-two-square

    No documentation

    Numbers equal to the sum of two square numbers
    keyword: number theory category: Mathematics/Arithmetic and Number Theory/Number theory date: 2004-12-13
    Laurent Thery
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  22. coq-switch

    No documentation

    A plugin to implement functionality similar to `switch` statement in C language
    category:Miscellaneous/Coq Extensions date:2023-12-13 logpath:Switch
    Vadim Zaliva <lord@crocodile.org>
    1.0.6
    MIT
    Used by 0 other packages
    13 Dec 2023
  23. coq-tactician

    No documentation

    Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq
    keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:Tactician
    Lasse Blaauwbroek <lasse@blaauwbroek.eu>
    1.0~beta2.1+8.19
    MIT
    Used by 1 other packages
    18 Jul 2024
  24. coq-tactician-api

    No documentation

    An API exposing Coq's web of formal knowledge to external agents
    Lasse Blaauwbroek <lasse@blaauwbroek.eu>
    15.0+8.11
    MIT
    Used by 2 other packages
    11 Jan 2024
  25. coq-tactician-dummy

    No documentation

    A dummy implementation of Tactician
    keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:Tactician
    Lasse Blaauwbroek <lasse@blaauwbroek.eu>
    1.0~beta2+8.17
    MIT
    Used by 1 other packages
    19 Oct 2023
  26. coq-tactician-stdlib

    No documentation

    Recompiles Coq's standard libary with Tactician's instrumentation loaded
    keyword:tactic-learning keyword:machine-learning keyword:automation keyword:proof-synthesis category:Miscellaneous/Coq Extensions logpath:Tactician
    Lasse Blaauwbroek <lasse@blaauwbroek.eu
    1.0~beta2+8.16
    MIT
    Used by 0 other packages
    19 Oct 2023
  27. coq-tait

    No documentation

    A normalization proof a la Tait for simply-typed lambda-calculus
    keyword: normalization keyword: lambda calculus keyword: extraction keyword: Tait proof keyword: normalization by evalution keyword: type theory category: Mathematics/Logic/Type theory category: Computer Science/Lambda Calculi category: Miscellaneous/Extracted Programs/Type checking unification and normalization date: 2004
    Pierre Letouzey Helmut Schwichtenberg
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  28. coq-tarski-geometry

    No documentation

    Tarski's geometry
    keyword: geometry keyword: Tarski's geometry keyword: congruence keyword: between property keyword: orthogonality category: Mathematics/Geometry/General date: 2006-03
    Julien Narboux <Julien.Narboux@dpt-info.u-strasbg.fr> [http://dpt-info.u-strasbg.fr/~narboux/]
    8.10.0
    GPL
    Used by 0 other packages
    07 Dec 2019
  29. coq-template-coq

    No documentation

    A quoting library for Coq
    Gregory Malecha
    1.1.0~beta3
    BSD
    Used by 0 other packages
    25 Nov 2015
  30. coq-text2tac

    No documentation

    Language model that predicts tactics for Tactician
    Jelle Piepenbrock
    1.0
    https://zenodo.org/records/10410474/files/LICENSE.md
    Used by 0 other packages
    11 Jan 2024
  31. coq-three-gap

    No documentation

    A Proof of the Three Gap Theorem (Steinhaus Conjecture)
    keyword: real numbers keyword: Steinhaus keyword: Three Gap Theorem category: Mathematics/Geometry category: Mathematics/Arithmetic and Number Theory/Miscellaneous
    Micaela Mayero
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  32. coq-tlc

    No documentation

    TLC: A Library for Classical Coq
    category:Computer Science/Data Types and Data Structures date:2024-02-09 keyword:classical logic logpath:TLC
    Arthur Charguéraud
    20240209
    MIT
    Used by 2 other packages
    13 Feb 2024
  33. coq-topology

    No documentation

    General topology in Coq
    category:Mathematics/Real Calculus and Topology date:2023-08-18 keyword:topology keyword:filters keyword:nets keyword:metric spaces keyword:real analysis keyword:Urysohn's lemma keyword:Tietze extension theorem logpath:Topology
    Daniel Schepler
    10.2.0
    LGPL-2.1-or-later
    Used by 0 other packages
    21 Aug 2023
  34. coq-tortoise-hare-algorithm

    No documentation

    Tortoise and the hare algorithm
    keyword: program verification keyword: paths keyword: cycle detection keyword: graphs keyword: graph theory keyword: finite sets keyword: Floyd category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms date: 2007-02
    Jean-Christophe Filliâtre
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  35. coq-trakt

    No documentation

    A generic goal preprocessing tool for proof automation tactics in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi date:2022-05-16 logpath:Trakt
    Enzo Crance
    1.2c
    LGPL-3.0-or-later
    Used by 0 other packages
    19 Jun 2024
  36. coq-traversable-fincontainer

    No documentation

    Traversable Functors are Finitary Containers
    keyword: finitary container keyword: traversable functors category: Computer Science/Data Types and Data Structures
    Russell O'Connor <oconnorr@google.com>
    8.10.0
    ASL
    Used by 0 other packages
    07 Dec 2019
  37. coq-tree-automata

    No documentation

    Tree automatas
    keyword: tree automatas keyword: bottom up reflexion terms category: Computer Science/Formal Languages Theory and Automata date: september 1999
    Xavier Rival [http://www.eleves.ens.fr/home/rival]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  38. coq-tree-calculus

    No documentation

    A Coq library for tree calculus
    keyword:tree calculus keyword:reflective programs category:Computer Science/Lambda Calculi date:2020-09-20 logpath:Reflective
    Barry Jay
    1.0.0
    MIT
    Used by 0 other packages
    21 Sep 2020
  39. coq-tree-diameter

    No documentation

    Diameter of a binary tree
    keyword: program verification keyword: trees keyword: paths keyword: graphs keyword: distance keyword: diameter category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
    Jean-Christophe Filliâtre
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  40. coq-trocq-hott

    No documentation

    A modular parametricity plugin for proof transfer in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:Trocq
    Cyril Cohen Enzo Crance Lucie Lahaye Assia Mahboubi
    0.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    01 Jul 2025
  41. coq-trocq-hott-examples

    No documentation

    A modular parametricity plugin for proof transfer in Coq: examples
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:Trocq
    Cyril Cohen Enzo Crance Lucie Lahaye Assia Mahboubi
    0.2.0
    LGPL-3.0-or-later
    Used by 0 other packages
    01 Jul 2025
  42. coq-trocq-std

    No documentation

    A modular parametricity plugin for proof transfer in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:Trocq
    Cyril Cohen Enzo Crance Lucie Lahaye Assia Mahboubi
    0.2.0
    LGPL-3.0-or-later
    Used by 1 other packages
    01 Jul 2025
  43. coq-trocq-std-examples

    No documentation

    A modular parametricity plugin for proof transfer in Coq: examples
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi keyword:proof transfer keyword:isomorphism keyword:univalence keyword:parametricity logpath:Trocq
    Cyril Cohen Enzo Crance Lucie Lahaye Assia Mahboubi
    0.2.0
    LGPL-3.0-or-later
    Used by 0 other packages
    01 Jul 2025
  44. coq-type-infer

    No documentation

    A formal verification of algorithm W
    Masayuki Mizuno <mizuno@wantedly.com>
    0.1.0
    MIT
    Used by 0 other packages
    15 Dec 2020
  45. coq-typing-flags

    No documentation

    A Coq plugin to disable positivity check, guard check and termination check
    keyword:non-termination keyword:type-in-type category:Miscellaneous/Coq Extensions date:2019-11-02 logpath:TypingFlags
    Simon Boulier
    1.0
    Unknown
    Used by 0 other packages
    02 Nov 2019
  46. coq-unicoq

    No documentation

    An enhanced unification algorithm for Coq
    logpath:Unicoq date:2024-11-22
    Matthieu Sozeau <matthieu.sozeau@inria.fr> Beta Ziliani <beta@mpi-sws.org>
    1.6+8.20
    MIT
    Used by 1 other packages
    22 Nov 2024
  47. coq-unimath

    No documentation

    Library of Univalent Mathematics
    The UniMath Development Team
    20250923
    Similar to MIT license
    Used by 0 other packages
    30 Sep 2025
  48. coq-unimath-category-theory

    No documentation

    Aims to formalize a substantial body of mathematics using the univalent point of view
    The UniMath Development Team
    0.1.0
    Kind of MIT
    Used by 2 other packages
    14 May 2019
  49. coq-unimath-dedekind

    No documentation

    Aims to formalize a substantial body of mathematics using the univalent point of view
    The UniMath Development Team
    0.1.0
    Kind of MIT
    Used by 0 other packages
    14 May 2019
  50. coq-unimath-foundations

    No documentation

    Aims to formalize a substantial body of mathematics using the univalent point of view
    The UniMath Development Team
    0.1.0
    Kind of MIT
    Used by 5 other packages
    14 May 2019
... 8 9 10 11