254 search results for "tag:"date:""

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-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
  3. 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
  4. 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
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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
  50. coq-diqt

    No documentation

    Formalization of hashtables with Radix trees and PArray
    keyword:hashtables keyword:primitive arrays keyword:data structures keyword:dictionaries category:Computer Science/Data Types and Data Structures logpath:Diqt date:2023-07-13
    Valeran Maytié <valeran.maytie@universite-paris-saclay.fr>
    1.0.0
    CECILL-B
    Used by 0 other packages
    13 Jul 2023
1 2 3 ... 6