522 search results for ""

Showing 351 - 400
  1. coq-pil

    No documentation

    Coq library for Propositional Intuitionistic Logic & Pitts Interpolation Library
    date:2025-02-14 keyword:intuitionistic logic keyword:proof theory keyword:propositional quantifiers category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Mathematics/Logic/Foundations category:Mathematics/Logic/Modal logic logpath:ISL
    Hugo Férée Sam van Gool Yago Iglesias Vasquez
    1.0.1
    CECILL-2.1
    Used by 0 other packages
    26 Feb 2025
  2. coq-plouffe

    No documentation

    A Coq formalization of Plouffe formula
    logpath:Plouffe
    Laurent Thery
    1.5.0
    MIT
    Used by 0 other packages
    19 Dec 2024
  3. coq-plugin-utils

    No documentation

    Utility functions for implementing Coq plugins, e.g. building natural
    logpath:PluginUtils
    Gregory Malecha
    1.3.0
    MIT
    Used by 3 other packages
    28 Jul 2017
  4. coq-pocklington

    No documentation

    Pocklington's criterion in Coq
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:Pocklington keyword:number theory keyword:prime numbers keyword:primality keyword:Fermat's little theorem logpath:Pocklington date:2021-01-01
    Olga Caprotti Martijn Oostdijk
    8.12.0
    LGPL-2.1-or-later
    Used by 1 other packages
    02 Jan 2021
  5. coq-poltac

    No documentation

    A set of tactics to deal with inequalities in Coq over N, Z and R:
    logpath:PolTac
    Laurent Théry
    0.8.12
    LGPL-2.1-only
    Used by 0 other packages
    27 Aug 2020
  6. coq-pprint

    No documentation

    A modern combinator pretty-printing library for Coq
    Mathis Bouverot-Dupuis
    0.2.1+8.20
    MIT
    Used by 0 other packages
    19 Nov 2024
  7. coq-ppsimpl

    No documentation

    Ppsimpl is a reflexive tactic for canonising (arithmetic) goals
    keyword:integers keyword:arithmetic keyword:automation category:Miscellaneous/Coq Extensions logpath:PP
    Frédéric Besson
    8.10.0
    LGPL 3
    Used by 0 other packages
    18 Oct 2019
  8. coq-presburger

    No documentation

    Presburger's algorithm
    keyword: integers keyword: arithmetic keyword: decision procedure keyword: Presburger category: Mathematics/Logic/Foundations category: Mathematics/Arithmetic and Number Theory/Miscellaneous category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures date: March 2002
    Laurent Théry
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  9. coq-prfx

    No documentation

    Proof Reflection in Coq
    keyword: first-order logic keyword: natural deduction keyword: reflection keyword: proof terms keyword: de Bruijn indices keyword: permutative conversions category: Mathematics/Logic/Foundations date: 15 April 2005
    Dimitri Hendriks <hendriks@cs.ru.nl> [http://www.cs.ru.nl/~hendriks/]
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  10. coq-printf

    No documentation

    Implementation of sprintf for Coq
    date:2020-04-05 logpath:Printf
    Gregory Malecha
    2.0.0
    MIT
    Used by 0 other packages
    06 Apr 2020
  11. coq-procrastination

    No documentation

    A small library for collecting side conditions and deferring their proof
    logpath:Procrastination
    Armaël Guéneau <armael.gueneau@inria.fr>
    1.2
    LGPL
    Used by 0 other packages
    18 Sep 2018
  12. coq-projective-geometry

    No documentation

    Projective Geometry
    keyword: geometry keyword: projective keyword: Fano keyword: homogeneous coordinates model keyword: flat keyword: rank keyword: Desargues keyword: Moulton category: Mathematics/Geometry/General date: 2009-10
    Nicolas Magaud <Nicolas.Magaud@lsiit-cnrs.unistra.fr> Julien Narboux <Julien.Narboux@lsiit-cnrs.unistra.fr> Pascal Schreck <Pascal.Schreck@lsiit-cnrs.unistra.fr>
    8.10.0
    GPL
    Used by 0 other packages
    07 Dec 2019
  13. coq-propcalc

    No documentation

    Propositional Calculus
    keyword: propositional calculus keyword: classical logic keyword: completeness keyword: natural deduction keyword: sequent calculus keyword: cut elimination category: Mathematics/Logic/Foundations
    Floris van Doorn <fpvdoorn@gmail.com> [http://www.contrib.andrew.cmu.edu/~fpv/]
    8.10.0
    BSD
    Used by 0 other packages
    07 Dec 2019
  14. coq-prosa

    No documentation

    A Foundation for Formally Proven Schedulability Analysis
    keyword:prosa keyword:real-time keyword:schedulability analysis keyword:response-time analysis logpath:prosa
    Felipe Cerqueira Björn Brandenburg Maxime Lesourd Sergey Bozhko Xiaojie Guo et al.
    0.5
    BSD-2-Clause
    Used by 0 other packages
    08 Nov 2022
  15. coq-pts

    No documentation

    A formalisation of Pure Type Systems
    keyword: pure type systems keyword: metatheory category: Computer Science/Lambda Calculi date: 2007-03
    Bruno Barras
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  16. coq-ptsatr

    No documentation

    PTSATR
    keyword: pure type systems keyword: judgmental equality keyword: Church-Rosser keyword: confluence keyword: subject reduction keyword: pi injectivity category: Mathematics/Logic/Type theory
    Vincent Siles <vincent.siles@ens-lyon.org> [http://www.lix.polytechnique.fr/~vsiles] Hugo Herbelin <hugo.herbelin@inria.fr> [http://pauillac.inria.fr/~herbelin/]
    8.10.0
    LGPL
    Used by 1 other packages
    07 Dec 2019
  17. coq-ptsf

    No documentation

    Explicit Convertibility Proofs in Pure Type Systems
    keyword: pure type systems keyword: judgmental equality keyword: explicit equality proofs keyword: proof relevance category: Mathematics/Logic/Type theory
    Floris van Doorn <fpv@andrew.cmu.edu> [http://www.andrew.cmu.edu/user/fpv/] Herman Geuvers <herman@cs.ru.nl> [http://www.cs.ru.nl/~herman/] Freek Wiedijk <freek@cs.ru.nl> [http://www.cs.ru.nl/~freek/]
    8.10.0
    BSD
    Used by 0 other packages
    07 Dec 2019
  18. coq-qarith

    No documentation

    A Library for Rational Numbers (QArith)
    keyword: Q keyword: arithmetic keyword: rational numbers keyword: setoid keyword: ring category: Mathematics/Arithmetic and Number Theory/Rational numbers category: Miscellaneous/Extracted Programs/Arithmetic
    Pierre Letouzey
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  19. coq-qarith-stern-brocot

    No documentation

    Binary rational numbers in Coq
    category:Mathematics/Arithmetic and Number Theory/Rational numbers category:Miscellaneous/Extracted Programs/Arithmetic keyword:rational numbers keyword:arithmetic keyword:field tactic keyword:binary lists keyword:Stern-Brocot logpath:QArithSternBrocot date:2023-10-15
    Milad Niqui Yves Bertot
    8.18.0
    LGPL-2.1-or-later
    Used by 0 other packages
    15 Oct 2023
  20. coq-qcert

    No documentation

    Verified compiler for data-centric languages
    keyword:databases keyword:queries keyword:relational keyword:compiler date:2020-08-22 logpath:Qcert
    Josh Auerbach <> Martin Hirzel <> Louis Mandel <> Avi Shinnar <> Jerome Simeon <>
    2.2.0
    Apache-2.0
    Used by 0 other packages
    22 May 2022
  21. coq-quantumlib

    No documentation

    Coq library for reasoning about quantum programs
    keyword:quantum keyword:qwire keyword:sqir keyword:matrices keyword:vectors keyword:linear algebra keyword:complex numbers category:Mathematics/Algebra category:Mathematics/Real Calculus and Topology date:2025-09-19 logpath:QuantumLib
    inQWIRE
    1.8.0
    MIT
    Used by 0 other packages
    14 Oct 2025
  22. coq-quickchick

    No documentation

    Randomized Property-Based Testing for Coq
    Leonidas Lampropoulos Zoe Paraskevopoulou Maxime Denes Catalin Hritcu Benjamin Pierce et al.
    2.1.1
    MIT
    Used by 3 other packages
    02 Jul 2025
  23. coq-quicksort-complexity

    No documentation

    Proofs of Quicksort's worst- and average-case complexity
    keyword: quicksort keyword: complexity keyword: average-case category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms date: 2010-06
    Eelis
    8.10.0
    BSD
    Used by 0 other packages
    07 Dec 2019
  24. coq-railroad-crossing

    No documentation

    The Railroad Crossing Example
    keyword: CTL keyword: TCTL keyword: real time keyword: timed automatas keyword: safety keyword: concurrency properties keyword: invariants keyword: non-Zeno keyword: discrete time category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols date: February-March 2000
    Carlos Daniel Luna [http://www.fing.edu.uy/~cluna]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  25. coq-ramsey

    No documentation

    Ramsey Theory
    keyword: dimension one Ramsey theorem keyword: constructive mathematics keyword: almost full sets category: Mathematics/Logic category: Mathematics/Combinatorics and Graph Theory category: Miscellaneous/Extracted Programs/Combinatorics
    Marc Bezem
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  26. coq-random

    No documentation

    Interpretation of random programs
    keyword: randomized algorithms keyword: monads keyword: probability category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
    Christine Paulin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  27. coq-rational

    No documentation

    A definition of rational numbers
    keyword: integers keyword: rational numbers keyword: quotient types keyword: subset types category: Mathematics/Arithmetic and Number Theory/Rational numbers
    Samuel Boutin
    8.6.0
    LGPL 2.1
    Used by 0 other packages
    12 May 2019
  28. coq-record-update

    No documentation

    Generic support for updating record fields in Coq
    category:Computer Science/Data Types and Data Structures keyword:record logpath:RecordUpdate date:2025-09-05
    Tej Chajed
    0.3.6
    MIT
    Used by 2 other packages
    08 Sep 2025
  29. coq-recursive-definition

    No documentation

    ML-like recursive definitions
    keyword: recursive functions keyword: well-foundedness category: Miscellaneous/Coq Extensions date: 2002
    Antonia Balaa Yves Bertot
    8.6.0
    LGPL 2.1
    Used by 0 other packages
    20 Nov 2018
  30. coq-reduction-effects

    No documentation

    A Coq plugin to add reduction side effects to some Coq reduction strategies
    logpath:ReductionEffect
    Hugo Herbelin
    0.1.6
    MPL-2.0
    Used by 0 other packages
    08 Sep 2025
  31. coq-reflexive-first-order

    No documentation

    Reflexive first-order proof interpreter
    keyword: computational reflection keyword: interpretation keyword: first-order logic keyword: equational reasoning category: Miscellaneous/Coq Extensions date: 2005-05
    Pierre Corbineau <pierre.corbineau@lri.fr> [http://www.cs.ru.nl/~corbineau]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  32. coq-regexp

    No documentation

    Regular Expression
    keyword: regular expressions keyword: Kleene algebra category: Computer Science/Formal Languages Theory and Automata
    Takashi Miyamoto <tmiya@bu.iij4u.or.jp> [http://study-func-prog.blogspot.com/]
    8.10.0
    LGPL
    Used by 0 other packages
    07 Dec 2019
  33. coq-regexp-brzozowski

    No documentation

    Decision procedures for regular expression equivalence in Coq using Mathematical Components
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Computer Science/Formal Languages Theory and Automata keyword:regular expressions keyword:decision procedure keyword:relation algebra logpath:RegexpBrzozowski date:2023-10-14
    Thierry Coquand Vincent Siles
    1.2
    MIT
    Used by 0 other packages
    14 Oct 2023
  34. coq-reglang

    No documentation

    Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp
    category:Computer Science/Formal Languages Theory and Automata keyword:regular languages keyword:regular expressions keyword:finite automata keyword:two-way automata keyword:monadic second-order logic logpath:RegLang date:2024-01-19
    Christian Doczkal Jan-Oliver Kaiser Gert Smolka
    1.2.2
    CECILL-B
    Used by 1 other packages
    10 May 2025
  35. coq-relation-algebra

    No documentation

    Compatibility package for rocq-relation-algebra
    Damien Pous <Damien.Pous@ens-lyon.fr>
    1.8.0
    LGPL-3.0-or-later
    Used by 2 other packages
    19 Sep 2025
  36. coq-relation-extraction

    No documentation

    Functions extraction from inductive relations
    keyword: extraction keyword: inductive relations keyword: semantics category: Computer Science/Semantics and Compilation/Compilation date: 2011
    Catherine Dubois, David Delahaye, Pierre-Nicolas Tollitte
    8.8.0
    Unknown
    Used by 0 other packages
    06 Feb 2019
  37. coq-rem

    No documentation

    Rem Theorem in Baire space
    keyword: Rem Theorem keyword: Baire space category: Mathematics/Real Calculus and Topology
    Henk Barendregt
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  38. coq-rewriter

    No documentation

    Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting, experimental and tailored for use in Fiat Cryptography
    logpath:Rewriter
    Google Inc. Massachusetts Institute of Technology
    0.0.12
    MIT OR Apache-2.0 OR BSD-1-Clause
    Used by 1 other packages
    06 Dec 2024
  39. coq-riscv

    No documentation

    RISC-V Specification in Coq, somewhat experimental
    logpath:riscv
    Massachusetts Institute of Technology
    0.0.6
    BSD-3-Clause
    Used by 1 other packages
    15 Oct 2025
  40. coq-robot

    No documentation

    Formal Foundations for Modeling Robot Manipulators
    keyword:robotics keyword:3D geometry logpath:robot date:2021-05-11
    Reynald Affeldt, AIST Cyril Cohen, Inria Laurent Thery, Inria
    0.1
    LGPL-2.1-or-later
    Used by 0 other packages
    11 May 2021
  41. coq-rsa

    No documentation

    Correctness of RSA algorithm
    keyword: RSA keyword: Chinese remainder keyword: Fermat's little theorem category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms date: 1999
    Jose C. Almeida Laurent Théry
    8.10.0
    LGPL-2.1-only
    Used by 0 other packages
    07 Dec 2019
  42. coq-ruler-compass-geometry

    No documentation

    Ruler and compass geometry axiomatization
    keyword: geometry keyword: plane geometry keyword: ruler and compass geometry keyword: Euclidian geometry keyword: Hilbert's axioms category: Mathematics/Geometry/General date: 2007-11
    Jean Duprat <Jean.Duprat@ens-lyon.fr>
    8.10.0
    GNU Lesser Public License
    Used by 0 other packages
    07 Dec 2019
  43. coq-rupicola

    No documentation

    Gallina to imperative code compilation, currently in design phase
    logpath:Rupicola
    Clément Pit-Claudel <clement.pitclaudel@live.com> Jade Philipoom Dustin Jamner Andres Erbsen Adam Chlipala
    0.0.11
    MIT
    Used by 0 other packages
    14 Oct 2025
  44. coq-rust-extraction

    No documentation

    Coq extraction to Rust
    keyword:rust keyword:extraction logpath:RustExtraction
    The COBRA team
    0.1.1
    MIT
    Used by 0 other packages
    23 May 2025
  45. coq-sail

    No documentation

    Support library for Sail, a language for describing the instruction semantics of processors
    logpath:Sail category:Computer Science/Semantics and Compilation/Semantics
    Alasdair Armstrong Thomas Bauereiss Brian Campbell Shaked Flur Jonathan French et al.
    0.20
    BSD-2-Clause
    Used by 0 other packages
    24 Oct 2025
  46. coq-sail-stdpp

    No documentation

    Support library for Sail, a language for describing the instruction semantics of processors, using stdpp bitvectors
    logpath:Sail category:Computer Science/Semantics and Compilation/Semantics
    Alasdair Armstrong Thomas Bauereiss Brian Campbell Shaked Flur Jonathan French et al.
    0.20
    BSD-2-Clause
    Used by 0 other packages
    24 Oct 2025
  47. coq-scev

    No documentation

    Proofs and simplification lemmas of an algebraic theory of recurrences
    keyword:mathematics category:Miscellaneous/Coq Extensions date:2016-09-01 logpath:coq-scev
    Siddharth Bhat
    1.0.1
    MIT
    Used by 0 other packages
    20 Nov 2018
  48. coq-schroeder

    No documentation

    The Theorem of Schroeder-Bernstein
    keyword: Schroeder-Bernstein keyword: set theory category: Mathematics/Logic/Set theory
    Hugo herbelin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  49. coq-search-trees

    No documentation

    Binary Search Trees
    keyword: binary search trees category: Computer Science/Data Types and Data Structures category: Miscellaneous/Extracted Programs/Data structures
    Pierre Castéran
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  50. coq-semantics

    No documentation

    A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation
    category:Computer Science/Semantics and Compilation/Semantics keyword:natural semantics keyword:denotational semantics keyword:axiomatic semantics keyword:Hoare logic keyword:Dijkstra weakest pre-condition calculus keyword:abstract interpretation keyword:intervals logpath:Semantics
    Yves Bertot
    8.14.0
    MIT
    Used by 0 other packages
    21 Nov 2021
... 7 8 9 ... 11