514 search results for ""

Showing 101 - 150
  1. 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
  2. coq-disel

    No documentation

    Core framework files for Disel, a separation-style logic for compositional verification of distributed systems in Coq
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:program verification keyword:separation logic keyword:distributed algorithms logpath:DiSeL.Core date:2022-11-28
    Ilya Sergey James R. Wilcox
    2.3
    BSD-2-Clause
    Used by 1 other packages
    28 Nov 2022
  3. coq-disel-examples

    No documentation

    Example systems for Disel, a separation-style logic for compositional verification of distributed systems in Coq
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:program verification keyword:separation logic keyword:distributed algorithms logpath:DiSeL.Examples date:2022-11-28
    Ilya Sergey James R. Wilcox
    2.3
    BSD-2-Clause
    Used by 0 other packages
    28 Nov 2022
  4. coq-distributed-reference-counting

    No documentation

    A Construction of Distributed Reference Counting
    keyword: garbage collection keyword: distributed algorithms category: Computer Science/Semantics and Compilation/Compilation category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols
    Luc Moreau, Jean Duprat
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  5. coq-domain-theory

    No documentation

    Elements of Domain Theory
    keyword: Concrete Domains category: Computer Science/Lambda Calculi
    Gilles Kahn
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  6. coq-dpdgraph

    No documentation

    Compute dependencies between Coq objects (definitions, theorems) and produce graphs
    category:Miscellaneous/Coq Extensions keyword:dependency graph keyword:dependency analysis logpath:dpdgraph date:2025-05-28
    Anne Pacalet Yves Bertot Olivier Pons
    1.0+9.0
    LGPL-2.1-only
    Used by 0 other packages
    29 May 2025
  7. coq-elm-extraction

    No documentation

    Coq extraction to Elm
    keyword:elm keyword:extraction logpath:ElmExtraction
    The COBRA team
    0.1.1
    MIT
    Used by 0 other packages
    23 May 2025
  8. coq-elpi

    No documentation

    Compatibility metapackage for Elpi extension language after the Rocq renaming
    category:Miscellaneous/Coq Extensions keyword:λProlog keyword:higher order abstract syntax logpath:elpi
    Enrico Tassi <enrico.tassi@inria.fr>
    3.1.0
    LGPL-2.1-or-later
    Used by 7 other packages
    02 Sep 2025
  9. coq-equations

    No documentation

    Compatibility package, see rocq-equations
    Matthieu Sozeau <matthieu.sozeau@inria.fr>
    1.3.1+9.0
    LGPL-2.1-only
    Used by 12 other packages
    20 Mar 2025
  10. coq-ergo

    No documentation

    Ergo: a Coq plugin for reification of term with arbitrary signature
    keyword: reflexive decision procedure keyword: satisfiability modulo theories category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures
    Stéphane Lescuyer
    8.6.0
    Unknown
    Used by 0 other packages
    20 Nov 2018
  11. coq-error-handlers

    No documentation

    Simple and robust error handling functions
    Guillaume Claret
    1.2.0
    MIT
    Used by 5 other packages
    25 Nov 2015
  12. coq-euclidean-geometry

    No documentation

    Basis of the Euclid's plane geometry
    keyword: plane geometry keyword: Euclid keyword: ruler and compass category: Mathematics/Geometry/General
    Jean Duprat <Jean.Duprat@ens-lyon.fr>
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  13. coq-euler-formula

    No documentation

    Hypermaps, Genus Theorem and Euler Formula
    keyword: polyhedron keyword: hypermap keyword: genus keyword: Euler formula keyword: assisted proofs category: Mathematics/Geometry date: 2006-09
    Jean-François Dufourd <dufourd@dpt-info.u-strasbg.fr> [http://dpt-info.u-strasbg.fr/~jfd/]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  14. coq-exact-real-arithmetic

    No documentation

    Exact Real Arithmetic
    keyword: correctness keyword: real numbers keyword: arithmetic category: Mathematics/Real Numbers
    Jérôme Creci
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  15. coq-exceptions

    No documentation

    Pro[gramm,v]ing with continuations:A development in Coq
    keyword: exceptions keyword: continuations category: Computer Science/Semantics and Compilation/Semantics
    Pierre Castéran
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  16. coq-ext-lib

    No documentation

    A library of Coq definitions, theorems, and tactics
    logpath:ExtLib
    Gregory Malecha
    0.13.0
    BSD-2-Clause
    Used by 14 other packages
    06 Dec 2024
  17. coq-extensible-records

    No documentation

    Definitional (canonical) extensible records in Coq with string keys and arbitrary (non-dependent) types
    Gregory Malecha
    1.2.0
    MIT
    Used by 0 other packages
    12 May 2019
  18. coq-extructures

    No documentation

    Finite sets, maps, and other data structures with extensional reasoning
    keyword:finite maps keyword:extensionality category:Computer Science/Data Types and Data Structures logpath:extructures
    Arthur Azevedo de Amorim
    0.5.0
    MIT
    Used by 1 other packages
    10 Dec 2024
  19. coq-fairisle

    No documentation

    Proof of the Fairisle 4x4 Switch Element
    keyword: circuits keyword: automata keyword: co-induction keyword: dependent types category: Computer Science/Architecture date: 2005-12-15
    Solange Coupet-Grimal <Solange.Coupet@lif.univ-mrs.fr> [http://www.cmi.univ-mrs.fr/~solange/] Line Jakubiec-Jamet <Line.Jakubiec@lif.univ-mrs.fr> [http://www.dil.univ-mrs.fr/~jakubiec/]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  20. coq-fcsl-pcm

    No documentation

    Coq library of Partial Commutative Monoids
    category:Computer Science/Data Types and Data Structures keyword:partial commutative monoids keyword:separation logic keyword:concurrency logpath:pcm
    Aleksandar Nanevski Anton Trunov Alexander Gryzlov
    2.2.0
    Apache-2.0
    Used by 4 other packages
    12 Jun 2025
  21. coq-fermat4

    No documentation

    Diophantus' 20th Problem and Fermat's Last Theorem for n = 4
    keyword: Diophantus keyword: Fermat keyword: arithmetic keyword: infinite descent category: Mathematics/Arithmetic and Number Theory/Number theory date: 2005-07
    David Delahaye Micaela Mayero
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  22. coq-fiat-crypto

    No documentation

    Cryptographic Primitive Code Generation by Fiat
    logpath:Crypto
    Andres Erbsen <andreser@mit.edu> Google Inc. Jade Philipoom <jadep@mit.edu> <jade.philipoom@gmail.com> Massachusetts Institute of Technology Zoe Paraskevopoulou <zoe.paraskevopoulou@gmail.com>
    0.1.3
    MIT OR Apache-2.0 OR BSD-1-Clause
    Used by 0 other packages
    22 Apr 2024
  23. coq-file-sync

    No documentation

    File synchroniser specification in Coq
    logpath:FileSync
    Yishuai Li <liyishuai.lys@alibaba-inc.com>
    0.1.0
    MPL-2.0
    Used by 0 other packages
    14 Sep 2022
  24. coq-finger-tree

    No documentation

    Dependent Finger Trees
    keyword: data structures keyword: dependent types keyword: Finger Trees category: Computer Science/Data Types and Data Structures date: 2009-02
    Matthieu Sozeau <mattam@mattam.org> [http://mattam.org]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  25. coq-finmatrix

    No documentation

    Matrix by fin (finite set over nat) in Coq
    keyword:matrices category:Mathematics/Algebra date:2024-06-11 logpath:FinMatrix
    ZhengPu Shi
    1.0.2
    MIT
    Used by 0 other packages
    11 Jun 2024
  26. coq-firing-squad

    No documentation

    Firing Squad Synchronization Problem
    keyword: concurrency keyword: synchronization keyword: finite-state machines category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols category: Miscellaneous/Extracted Programs/Automata and protocols
    Jean Duprat
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  27. coq-float

    No documentation

    Library for floating-point numbers
    keyword: floating-point arithmetic category: Computer Science/Data Types and Data Structures date: 2001
    Laurent Théry Sylvie Boldo
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  28. coq-flocq

    No documentation

    A formalization of floating-point arithmetic for the Coq system
    keyword:floating-point arithmetic logpath:Flocq date:2025-01-26
    Sylvie Boldo <sylvie.boldo@inria.fr> Guillaume Melquiond <guillaume.melquiond@inria.fr>
    4.2.1
    LGPL-3.0-or-later
    Used by 18 other packages
    26 Jan 2025
  29. coq-flocq-quickchick

    No documentation

    Flocq binary_float generators for QuickChick testing framework
    logpath: FlocqQuickChick date: 2020-04-01
    Yaroslav Kogevnikov <ykozhevnikov@codeminders.com>
    1.0.2
    MIT
    Used by 0 other packages
    03 Apr 2020
  30. coq-formalv-check_range

    No documentation

    Tactics to automatically prove Boolean goals involving Uint63/Sint63 variables
    keyword:automation keyword:primitive integers logpath:formalv.check_range
    Ana de Almeida Borges Quim Casals Buñuel Juan Conejero Rodriguez Mireia González Bedmar Eduardo Hermo Reyes
    1.3.1
    PolyForm Noncommercial License 1.0.0
    Used by 1 other packages
    13 May 2025
  31. coq-formalv-prim63_mathcomp

    No documentation

    Refinements from MathComp nat and int to Coq primitive integers Uint63/Sint63
    keyword:refinement keyword:primitive integers logpath:formalv.prim63_mathcomp
    Ana de Almeida Borges Quim Casals Buñuel Juan Conejero Rodriguez Mireia González Bedmar Eduardo Hermo Reyes
    1.3.1
    PolyForm Noncommercial License 1.0.0
    Used by 2 other packages
    13 May 2025
  32. coq-formalv-time

    No documentation

    A Coq library for time and date arithmetic according to the UTC standard with leap seconds
    keyword:time keyword:date keyword:timestamp keyword:coq formalization logpath:formalv.time
    Ana de Almeida Borges Quim Casals Buñuel Juan Conejero Rodriguez Mireia González Bedmar Eduardo Hermo Reyes
    1.3.1
    PolyForm Noncommercial License 1.0.0
    Used by 0 other packages
    13 May 2025
  33. coq-founify

    No documentation

    Correctness and extraction of the unification algorithm
    keyword: First-order Unification keyword: Robinson category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category: Miscellaneous/Extracted Programs/Type checking unification and normalization
    Jocelyne Rouyer
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  34. coq-fourcolor

    No documentation

    Mechanization of the Four Color Theorem in Coq
    category:Mathematics/Combinatorics and Graph Theory keyword:Four color theorem keyword:small scale reflection keyword:Mathematical Components logpath:fourcolor.proof date:2025-04-16
    Georges Gonthier
    1.4.1
    CECILL-B
    Used by 1 other packages
    21 Apr 2025
  35. coq-fourcolor-reals

    No documentation

    Interface for real numbers used in the Four Color Theorem
    category:Mathematics/Real Calculus and Topology keyword:real numbers logpath:fourcolor.reals date:2025-04-16
    Georges Gonthier
    1.4.1
    CECILL-B
    Used by 2 other packages
    21 Apr 2025
  36. coq-fpmods

    No documentation

    A short constructive formalization of finitely presented modules
    logpath:fpmods
    Cyril Cohen and Anders Mörtberg
    0.2.0
    MIT
    Used by 0 other packages
    25 Nov 2015
  37. coq-free-groups

    No documentation

    Free Groups
    keyword: free group category: Mathematics/Algebra
    Daniel Schepler <dschepler@gmail.com>
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  38. coq-freesim

    No documentation

    Stuttering For Free
    keyword:simulation keyword:coinduction keyword:dual non-determinism keyword:up to techniques keyword:companion keyword:Interaction Trees keyword:CompCert logpath:FreeSim
    Minki Cho, Youngju Song, Dongjae Lee
    1.0.0
    BSD-3-Clause
    Used by 0 other packages
    19 Sep 2023
  39. coq-freespec-core

    No documentation

    A framework for implementing and certifying impure computations in Coq
    date:2021-03-01 keyword:effects keyword:freer keyword:program logic category:Mathematics/Category Theory logpath:FreeSpec.Core
    Thomas Letan Yann Régis-Gianas
    0.3
    MPL-2.0
    Used by 2 other packages
    04 Mar 2021
  40. coq-freespec-exec

    No documentation

    A framework for implementing and certifying impure computations in Coq
    date:2021-03-01 keyword:plugin category:Miscellaneous/Coq Extensions logpath:FreeSpec.Exec
    Thomas Letan Yann Régis-Gianas
    0.3
    MPL-2.0
    Used by 0 other packages
    04 Mar 2021
  41. coq-freespec-ffi

    No documentation

    A framework for implementing and certifying impure computations in Coq
    date:2021-03-01 keyword:foreign function interface category:Miscellaneous/Coq Extensions logpath:FreeSpec.FFI
    Thomas Letan Yann Régis-Gianas
    0.3
    MPL-2.0
    Used by 1 other packages
    04 Mar 2021
  42. coq-friedman-tree

    No documentation

    Implementation of Friedman's TREE function based on Kruskal's theorem
    category:Computer Science/Data Types and Data Structures date:2024-05-23 logpath:FriedmanTREE
    Dominique Larchey-Wendling (https://github.com/DmxLarchey)
    1.1
    MPL-2.0
    Used by 0 other packages
    23 May 2024
  43. coq-fsets

    No documentation

    Finite Sets overs Ordered Types
    keyword: finite sets keyword: sorted lists keyword: balanced trees keyword: red-black trees keyword: AVL keyword: functors keyword: data structures category: Computer Science/Data Types and Data Structures category: Miscellaneous/Extracted Programs/Data structures
    Pierre Letouzey Jean-Christophe Filliâtre
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  44. coq-fssec-model

    No documentation

    Formal verification of an extension of a UNIX compatible, secure filesystem
    keyword: security keyword: filesystem keyword: UNIX keyword: MLS keyword: access control category: Computer Science/Operating Systems date: 2002-04-24
    Maximiliano Cristiá
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  45. coq-function-ninjas

    No documentation

    Simple functional combinators
    Guillaume Claret
    1.0.0
    MIT
    Used by 8 other packages
    25 Nov 2015
  46. coq-functional-algebra

    No documentation

    This package provides a Coq formalization of abstract algebra using
    keyword:algebra keyword:abstract algebra category:Miscellaneous/Coq Extensions date:2018-08-11 logpath:functional-algebra
    Larry D. Lee Jr.
    1.0.2
    LGPL-3.0
    Used by 0 other packages
    24 Aug 2018
  47. coq-functions-in-zfc

    No documentation

    Functions in classical ZFC
    keyword: set theory keyword: Zermelo-Fraenkel keyword: functions category: Mathematics/Logic/Set theory date: April 2001
    Carlos Simpson <carlos@math.unice.fr>
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  48. coq-fundamental-arithmetics

    No documentation

    Fundamental theorems of arithmetic
    keyword: arithmetic keyword: number theory category: Mathematics/Arithmetic and Number Theory/Miscellaneous date: 2008-02-1
    Sébastien Briais <sebastien.briais at ens-lyon.fr> [http://perso.ens-lyon.fr/sebastien.briais/]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  49. coq-gaia

    No documentation

    Implementation of books from Bourbaki's Elements of Mathematics in Coq
    category:Mathematics/Logic/Set theory keyword:Bourbaki keyword:set theory logpath:gaia date:2021-10-28
    José Grimm Alban Quadrat Carlos Simpson
    1.13
    MIT
    Used by 1 other packages
    30 Oct 2021
  50. coq-gaia-hydras

    No documentation

    Bridge in Coq between Gaia and Hydra battles
    category:Mathematics/Logic/Foundations keyword:ordinal numbers logpath:gaia_hydras date:2022-05-20
    Pierre Castéran
    0.9
    MIT
    Used by 0 other packages
    25 May 2022
2 3 4 ... 11