522 search results for ""

Showing 1 - 50
  1. coq-aac-tactics

    No documentation

    Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:reflexive tactic keyword:rewriting keyword:rewriting modulo associativity and commutativity keyword:rewriting modulo ac keyword:decision procedure logpath:AAC_tactics date:2024-06-27
    Thomas Braibant Damien Pous Fabian Kunze
    8.20.0
    LGPL-3.0-or-later
    Used by 2 other packages
    06 Sep 2024
  2. coq-abp

    No documentation

    A verification of the alternating bit protocol expressed in CBS
    keyword: alternating bit protocol keyword: process calculi keyword: reactive systems keyword: co-inductive types keyword: co-induction category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols
    Eduardo Giménez
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  3. coq-actuary

    No documentation

    Formalization of actuarial mathematics in Coq
    category:Mathematics/Real Calculus and Topology keyword:present value keyword:life tables keyword:annuities keyword:reserves keyword:actuarial mathematics logpath:Actuary date:2023-11-11
    Yosuke Ito
    2.6
    MIT
    Used by 0 other packages
    11 Nov 2023
  4. coq-addition-chains

    No documentation

    Exponentiation algorithms following addition chains in Coq
    category:Mathematics/Combinatorics and Graph Theory keyword:addition chains keyword:exponentiation algorithms logpath:additions date:2022-05-20
    Pierre Castéran Yves Bertot
    0.9
    MIT
    Used by 0 other packages
    25 May 2022
  5. coq-additions

    No documentation

    Addition Chains
    keyword: addition chains category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category: Miscellaneous/Extracted Programs/Arithmetic
    Pierre Castéran
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  6. coq-ails

    No documentation

    Proof of AILS algorithm
    keyword: ails keyword: aircraft keyword: trajectory keyword: conflict keyword: collision category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms date: 2002
    Olivier Desmettre
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  7. coq-alea

    No documentation

    Coq library for reasoning on randomized algorithms
    category:Computer Science/Data Types and Data Structures keyword:randomized algorithm keyword:probability keyword:monads logpath:ALEA
    Christine Paulin-Mohring David Baelde Pierre Courtieu
    8.12.0
    LGPL-2.1-only
    Used by 0 other packages
    03 Nov 2021
  8. coq-algebra

    No documentation

    Basics notions of algebra
    keyword: algebra category: Mathematics/Algebra date: 1999-03
    Loïc Pottier [http://www-sop.inria.fr/croap/personnel/Loic.Pottier/home.html]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  9. coq-algorand

    No documentation

    A verified model of the Algorand consensus protocol in Coq
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:distributed algorithms keyword:blockchain keyword:consensus keyword:algorand logpath:Algorand date:2022-11-20
    Musab A. Alturki Jing Chen Victor Luchangco Brandon Moore Karl Palmskog et al.
    1.4
    NCSA
    Used by 0 other packages
    21 Nov 2022
  10. coq-almost-full

    No documentation

    Almost-full relations in Coq for proving termination
    category:Computer Science/Data Types and Data Structures keyword:Ramsey theorem keyword:termination keyword:almost-full relations keyword:well-founded relations logpath:AlmostFull date:2023-12-28
    Dimitrios Vytiniotis Thierry Coquand David Wahlstedt
    8.18.0
    MIT
    Used by 0 other packages
    28 Dec 2023
  11. coq-amm11262

    No documentation

    Problem 11262 of The American Mathematical Monthly
    keyword: american mathematical monthly problem 11262 date: 2007-04
    Milad Niqui (Coq files) <milad@cs.ru.nl> [http://www.cs.ru.nl/~milad] Tonny Hurkens (paper proof) <hurkens@sci.kun.nl>
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  12. coq-angles

    No documentation

    Formalization of the oriented angles theory
    keyword: Pcoq keyword: geometry keyword: plane geometry keyword: oriented angles category: Mathematics/Geometry/General date: 2002-01-15
    Frédérique Guilhot <Frederique.Guilhot@sophia.inria.fr>
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  13. coq-antivalence

    No documentation

    A Coq plugin to generate type-inequality axioms for inductive definitions
    category:Miscellaneous/Coq Extensions logpath:Antivalence date:2020-08-24
    Isaac van Bakel
    1.0.1
    MIT
    Used by 0 other packages
    24 Aug 2020
  14. coq-approx-models

    No documentation

    Rigorous approximations with a posteriori verified operations
    category:Mathematics/Approximation Theory keyword:approximation theory keyword:Chebyshev polynomials keyword:certificate-based approximation logpath:ApproxModels date:2021-06-15
    Florent Bréhard Assia Mahboubi Damien Pous
    1.0
    CECILL-B
    Used by 0 other packages
    16 Jun 2021
  15. coq-area-method

    No documentation

    The Chou, Gao and Zhang area method
    keyword: geometry keyword: Chou Gao Zhang area method keyword: decision procedure keyword: automatic theorem proving date: 2004-2010
    Julien Narboux
    8.10.0
    Unknown
    Used by 0 other packages
    19 Oct 2020
  16. coq-async-test

    No documentation

    Testing asynchronous system
    category:Miscellaneous/Extracted Programs/Decision procedures keyword:extraction keyword:reactive systems logpath:AsyncTest
    Yishuai Li <yishuai@cis.upenn.edu>
    0.1.0
    MPL-2.0
    Used by 2 other packages
    29 May 2022
  17. coq-atbr

    No documentation

    Coq library and tactic for deciding Kleene algebras
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:Kleene algebra keyword:finite automata keyword:semiring keyword:matrices keyword:decision procedure keyword:reflexive tactic logpath:ATBR date:2024-06-30
    Thomas Braibant Damien Pous
    8.20.0
    LGPL-3.0-or-later
    Used by 0 other packages
    06 Sep 2024
  18. coq-automata

    No documentation

    Beginning of formal language theory
    keyword: formal language theory keyword: finite automata keyword: push-down automata keyword: rational langages keyword: Kleene category: Computer Science/Formal Languages Theory and Automata date: June-July 1993
    Judicaël Courant Jean-Christophe Filliâtre
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  19. coq-autosubst

    No documentation

    Coq library for parallel de Bruijn substitutions
    category:Computer Science/Lambda Calculi keyword:abstract syntax keyword:binders keyword:de Bruijn indices keyword:substitution logpath:Autosubst date:2024-07-12
    Steven Schäfer Tobias Tebbi
    1.9
    MIT
    Used by 0 other packages
    13 Jul 2024
  20. coq-autosubst-ocaml

    No documentation

    OCaml implementation of Autosubst 2 for Coq
    Adrian Dapprich
    1.1+8.20
    MIT
    Used by 0 other packages
    17 Jan 2025
  21. coq-axiomatic-abp

    No documentation

    Verification of an axiomatisation of the Alternating Bit Protocol
    keyword: Alternating Bit Protocol keyword: Process Calculi keyword: reactive systems category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols
    Jan Friso Groote
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  22. coq-bbv

    No documentation

    An implementation of bitvectors in Coq.
    Tej Chajed Haogang Chen Adam Chlipala Joonwon Choi Andres Erbsen et al.
    1.5
    MIT
    Used by 1 other packages
    07 Mar 2024
  23. coq-bdds

    No documentation

    BDD algorithms and proofs in Coq, by reflection
    keyword: BDD keyword: binary decision diagrams keyword: classical logic keyword: propositional logic keyword: validity keyword: satisfiability keyword: model checking keyword: reflection category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category: Miscellaneous/Extracted Programs/Decision procedures date: May-July 1999
    Kumar Neeraj Verma
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  24. coq-bedrock2

    No documentation

    A work-in-progress language and compiler for verified low-level programming
    logpath:bedrock2
    Massachusetts Institute of Technology Kevix SiFive
    0.0.9
    MIT
    Used by 2 other packages
    09 Oct 2025
  25. coq-bedrock2-compiler

    No documentation

    A work-in-progress language and compiler for verified low-level programming (compiler part)
    logpath:bedrock2
    Massachusetts Institute of Technology Kevix SiFive
    0.0.9
    MIT
    Used by 0 other packages
    29 Oct 2025
  26. coq-belgames

    No documentation

    BelGames: A Formal Theory of Games of Incomplete Information Based on Non-Monotonic Capacities in the Coq Proof Assistant
    keyword:games of incomplete information keyword:belief functions theory keyword:imprecise probability theory category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms logpath:BelGames date:2023-11-26
    Pierre Pomeret-Coquot Erik Martin-Dorel Hélène Fargier
    2.0.0
    MIT
    Used by 0 other packages
    06 Nov 2023
  27. coq-bellantonicook

    No documentation

    Deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions
    category:Computer Science/Algorithms/Complexity keyword:implicit complexity keyword:polynomial time logpath:BellantoniCook date:2018-09-06
    Sylvain Heraud David Nowak
    1.0.0
    CeCILL-A
    Used by 1 other packages
    07 Sep 2018
  28. coq-bertrand

    No documentation

    Correctness of Knuth's algorithm for prime numbers
    category:Mathematics/Arithmetic and Number Theory/Number theory category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs based on external tools category:Miscellaneous/Extracted Programs/Arithmetic keyword:Knuth's algorithm keyword:prime numbers keyword:Bertrand's postulate logpath:Bertrand date:2020-10-10
    Laurent Théry
    8.12.0
    LGPL-2.1-or-later
    Used by 0 other packages
    11 Oct 2020
  29. coq-bignums

    No documentation

    Compatibility wrapper for rocq-bignums
    category:Miscellaneous/Coq Extensions category:Mathematics/Arithmetic and Number Theory/Number theory category:Mathematics/Arithmetic and Number Theory/Rational numbers keyword:integer numbers keyword:rational numbers keyword:arithmetic keyword:arbitrary-precision logpath:Bignums
    Laurent Théry Benjamin Grégoire Arnaud Spiwack Evgeny Makarov Pierre Letouzey
    9.0.0+rocq9.1
    LGPL-2.1-only
    Used by 10 other packages
    16 Sep 2025
  30. coq-bits

    No documentation

    A bit vector library
    category:Computer Science/Data Types and Data Structures keyword:bit arithmetic keyword:bitset keyword:bit vector keyword:extraction logpath:Bits date:2021-07-11
    Andrew Kennedy <akenn@microsoft.com> Arthur Blot <arthur.blot@ens-lyon.fr> Pierre-Évariste Dagand <pierre-evariste.dagand@lip6.fr>
    1.1.0
    Apache-2.0
    Used by 0 other packages
    12 Jul 2021
  31. coq-bonsai

    No documentation

    Generate a fresh Bonsai on your terminal
    category:Miscellaneous/Logical Puzzles and Entertainment keyword:bonsai keyword:effects keyword:extraction date:2021-10-04
    Guillaume Claret
    1.0.0
    GPL-3.0-only
    Used by 0 other packages
    04 Oct 2021
  32. coq-buchberger

    No documentation

    Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases
    category:Mathematics/Algebra category:Miscellaneous/Extracted Programs/Combinatorics keyword:Gröbner basis keyword:polynomial ideal keyword:Buchberger's algorithm logpath:Buchberger date:2023-12-28
    Laurent Théry Henrik Persson
    8.18.0
    LGPL-2.1-or-later
    Used by 0 other packages
    28 Dec 2023
  33. coq-bytestring

    No documentation

    A simple string library built around byte instead of Ascii
    Gregory Malecha
    0.9.0
    LGPL-2.1 + BedRock
    Used by 0 other packages
    02 Jun 2020
  34. coq-canon-bdds

    No documentation

    Canonicity of Binary Decision Dags
    keyword: BDD keyword: BDT keyword: finite sets keyword: model checking keyword: binary decision diagrams category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category: Miscellaneous/Extracted Programs/Decision procedures
    Emmanuel Ledinot
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  35. coq-cantor

    No documentation

    On Ordinal Notations
    keyword: ordinal numbers keyword: well-foundedness keyword: termination keyword: rpo keyword: Goodstein sequences category: Mathematics/Logic category: Mathematics/Arithmetic and Number Theory/Number theory date: 2006-05-22
    Pierre Castéran <pierre.casteran@labri.fr> [http://www.labri.fr/~casteran/] Évelyne Contejean <contejea@lri.fr> [http://www.lri.fr/~contejea]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  36. coq-category-theory

    No documentation

    An axiom-free formalization of category theory in Coq
    keyword: category theory category: Mathematics/Category Theory date: 2022-07-22 logpath: Category
    John Wiegley
    1.0.0
    BSD-3-Clause
    Used by 0 other packages
    22 Jul 2022
  37. coq-cats-in-zfc

    No documentation

    Category theory in ZFC
    keyword: set theory keyword: ordinal numbers keyword: cardinal numbers keyword: category theory keyword: functors keyword: natural transformation keyword: limit keyword: colimit category: Mathematics/Logic/Set theory category: Mathematics/Category Theory date: 2004-10-10
    Carlos Simpson <carlos@math.unice.fr> [http://math.unice.fr/~carlos/]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  38. coq-ccs

    No documentation

    Equivalence notions on labelled transitions systems
    keyword: Labelled Transitions Systems keyword: process algebras keyword: Calculus of Concurrent Process (CCS) category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems
    Solange Coupet-Grimal
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  39. coq-cds4ltl

    No documentation

    A Calculational Deductive System for Linear Temporal Logic
    keyword: temporal logic category: Mathematics/Logic/Modal logic date: 2022-07-23 logpath: CDS4LTL
    John Wiegley
    1.0.0
    BSD-3-Clause
    Used by 0 other packages
    23 Jul 2022
  40. coq-cecoa

    No documentation

    Implicit-complexity Coq library to prove that some programs are computable in polynomial time
    category:Computer Science/Algorithms/Complexity keyword:implicit complexity keyword:polynomial time keyword:rewriting logpath:Cecoa date:2018-09-10
    Hugo Férée Samuel Hym Micaela Mayero Jean-Yves Moyen David Nowak
    1.0.0
    CeCILL-A
    Used by 0 other packages
    13 Sep 2018
  41. coq-ceramist

    No documentation

    Coq library for reasoning about probabilistic algorithms
    category:Computer Science/Data Types and Data Structures keyword: bloomfilter keyword: probability keyword: amq date:2020-04-06
    Kiran Gopinathan Ilya Sergey
    1.0.1
    GPL-3.0-or-later
    Used by 0 other packages
    06 Apr 2020
  42. coq-ceres

    No documentation

    Library for serialization to S-expressions
    logpath:Ceres keyword:serialization
    Li-yao Xia
    0.4.1
    MIT
    Used by 5 other packages
    03 Jul 2023
  43. coq-certicoq

    No documentation

    A Verified Compiler for Gallina, Written in Gallina
    Andrew Appel Yannick Forster Anvay Grover Joomy Korkut John Li et al.
    0.9+8.19
    MIT
    Used by 0 other packages
    04 Jun 2024
  44. coq-cfgv

    No documentation

    Generic Proofs about Alpha Equality and Substitution
    keyword: generic programming keyword: variable bindings keyword: context free grammars keyword: substitution keyword: alpha equality keyword: equivariance category: Computer Science/Lambda Calculi
    Abhishek <abhishek.anand.iitg@gmail.com> [http://www.cs.cornell.edu/~aa755/] Vincent Rahli <vincent.rahli@gmail.com> [http://www.cs.cornell.edu/~rahli/]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  45. coq-cfml

    No documentation

    The CFML program verification system
    date: logpath:CFML category:Computer Science/Programming Languages/Formal Definitions and Theory keyword:program verification keyword:separation logic keyword:weakest precondition
    Arthur Charguéraud
    20220112
    CC-BY-4.0
    Used by 0 other packages
    12 Jan 2022
  46. coq-cfml-basis

    No documentation

    The CFML Basis library
    date: logpath:CFML category:Computer Science/Programming Languages/Formal Definitions and Theory keyword:program verification keyword:separation logic keyword:weakest precondition
    Arthur Charguéraud
    20220112
    CC-BY-4.0
    Used by 2 other packages
    12 Jan 2022
  47. coq-cfml-stdlib

    No documentation

    The CFML standard library
    date: logpath:CFML.Stdlib category:Computer Science/Programming Languages/Formal Definitions and Theory keyword:program verification keyword:separation logic keyword:weakest precondition
    Arthur Charguéraud
    20220112
    CC-BY-4.0
    Used by 1 other packages
    12 Jan 2022
  48. coq-chapar

    No documentation

    A framework for verification of causal consistency for distributed key-value stores and their clients in Coq
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:causal consistency keyword:key-value stores keyword:distributed algorithms keyword:program verification logpath:Chapar date:2023-12-28
    Mohsen Lesani Christian J. Bell Adam Chlipala
    8.17.0
    MIT
    Used by 0 other packages
    28 Dec 2023
  49. coq-charge-core

    No documentation

    A framework of typeclasses for shallow embeddings of intuitionistic
    Jesper Bengtson Gregory Malecha
    1.2.0
    APACHE 2.0
    Used by 0 other packages
    28 Jul 2017
  50. coq-checker

    No documentation

    The Mutilated Checkerboard
    keyword: checker keyword: dominos keyword: puzzles category: Miscellaneous/Logical Puzzles and Entertainment
    Gérard Huet
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
1 2 3 ... 11