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

Showing 151 - 200
  1. coq-mathcomp-apery

    No documentation

    A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:apery recurrence keyword:irrationality keyword:creative telescoping logpath:mathcomp.apery date:2022-05-05
    Frédéric Chyzak Assia Mahboubi Thomas Sibut-Pinote
    1.0.2
    CECILL-C
    Used by 0 other packages
    05 May 2022
  2. coq-mathcomp-real-closed

    No documentation

    Mathematical Components Library on real closed fields
    keyword:real closed field logpath:mathcomp.real_closed date:2024-12-09
    Cyril Cohen Assia Mahboubi
    2.0.3
    CECILL-B
    Used by 5 other packages
    10 May 2025
  3. coq-mathcomp-tarjan

    No documentation

    Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp
    category:Computer Science/Graph Theory keyword:strongly connected components keyword:topological sorting keyword:Kosaraju keyword:Tarjan keyword:acyclicity keyword:graph theory logpath:mathcomp.tarjan date:2023-08-06
    Cyril Cohen Jean-Jacques Lévy Karl Palmskog Laurent Théry
    1.0.3
    CECILL-B
    Used by 0 other packages
    10 May 2025
  4. coq-mathcomp-word

    No documentation

    Yet Another Coq Library on Machine Words
    category:Computer Science/Data Types and Data Structures keyword:machine words logpath:mathcomp.word date:2024-03-21
    Pierre-Yves Strub
    3.2
    MIT
    Used by 1 other packages
    11 Jun 2024
  5. coq-matrices

    No documentation

    Ring properties for square matrices
    keyword: matrices keyword: vectors keyword: linear algebra keyword: Coq modules category: Mathematics/Algebra date: 2003-03
    Nicolas Magaud
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  6. coq-matrix

    No documentation

    Formal matrix theory with multiple implementations in Coq
    keyword:matrices category:Mathematics/Algebra date:2024-01-16 logpath:CoqMatrix
    ZhengPu Shi
    1.0.6
    MIT
    Used by 0 other packages
    16 Jan 2024
  7. coq-menhirlib

    No documentation

    A support library for verified Coq parsers produced by Menhir
    date:2025-09-12 logpath:MenhirLib
    Jacques-Henri Jourdan <jacques-henri.jourdan@lri.fr>
    20250912
    LGPL-3.0-or-later
    Used by 5 other packages
    16 Sep 2025
  8. coq-mi-cho-coq

    No documentation

    A specification of Michelson in Coq to prove properties about smart contracts in Tezos
    category:Computer Science/Programming Languages/Formal Definitions and Theory date:2021-06-15 keyword:cryptocurrency keyword:michelson keyword:semantics keyword:smart-contract keyword:tezos logpath:Michocoq logpath:Michocott
    Raphaël Cauderlier Bruno Bernardo Julien Tesson Arvid Jakobsson
    1.0.0
    MIT
    Used by 0 other packages
    21 Jun 2021
  9. coq-min-imports

    No documentation

    This script will try to remove unnecessary module imports from Coq
    category:Miscellaneous/Coq Extensions date:2018-04-22
    Vadim Zaliva
    1.0.2
    MIT
    Used by 0 other packages
    26 Apr 2018
  10. coq-mini-compiler

    No documentation

    Correctness of a tiny compiler for arithmetic expressions
    keyword: compilation keyword: correctness keyword: arithmetic category: Computer Science/Semantics and Compilation/Compilation date: 2003
    Jean-Christophe Filliâtre
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  11. coq-mk-choice-axiom-and-equivalent-propositions

    No documentation

    Machine-Proof-of-the-Axiom-of-Choice-and-Its-Equivalent-Propositions
    keyword:set theory keyword:choice axiom keyword:Morse-Kelley keyword:MK category:Mathematics/Logic/Set theory date:2025-02-28 logpath:MKACs
    Wensheng Yu Tianyu Sun Yaoshun Fu Sheng Yan Si Chen et al.
    1.0.0
    LGPL-2.1-only
    Used by 0 other packages
    28 Feb 2025
  12. coq-mk-reals-axioms

    No documentation

    A Coq formalization of the axiomatic definition of real numbers
    keyword:set theory keyword:Morse-Kelley keyword:MK real numbers category:Mathematics/Logic/Set theory date:2024-08-22 logpath:MKReals
    Wensheng Yu Dakai Guo Si Chen Guowei Dou Shukun Len
    1.0.0
    LGPL-2.1-only
    Used by 0 other packages
    28 Aug 2024
  13. coq-mmaps

    No documentation

    Several implementations of finite maps over arbitrary ordered types using Coq functors
    category:Computer Science/Data Types and Data Structures keyword:finite maps keyword:red-black trees keyword:AVL trees keyword:ordered types logpath:MMaps date:2024-01-08
    Pierre Letouzey Andrew W. Appel
    1.1
    LGPL-2.1-only
    Used by 0 other packages
    08 Jan 2024
  14. coq-mod-red

    No documentation

    Efficient Reduction of Large Integers by Small Moduli
    keyword: Algorithms keyword: Performance keyword: Computer Arithmetic keyword: Modular Reduction keyword: Optimization category: Mathematics/Arithmetic and Number Theory/Miscellaneous date: 2007-12; Updated in April 2009
    Luc Rutten
    8.10.0
    GNU Lesser General Public License
    Used by 0 other packages
    07 Dec 2019
  15. coq-moment

    No documentation

    Parse, manipulate and pretty-print times and dates in Coq
    date:2020-03-16 keyword:date keyword:time logpath:Moment
    Guillaume Claret
    1.2.1
    MIT
    Used by 3 other packages
    31 Oct 2021
  16. coq-monae

    No documentation

    Monads and equational reasoning in Coq
    keyword:monae keyword:effects keyword:probability keyword:nondeterminism logpath:monae date:2025-07-19
    Reynald Affeldt David Nowak Takafumi Saikawa Jacques Garrigue Ayumu Saito et al.
    0.9.1
    LGPL-2.1-or-later
    Used by 0 other packages
    23 Jul 2025
  17. coq-morse-kelley-axiomatic-set-theory

    No documentation

    A Coq formalization of the Morse-Kelley axiomatic set theory
    keyword:set theory keyword:axiomatic set theory keyword:Morse-Kelley keyword:MK category:Mathematics/Logic/Set theory date:2024-07-24 logpath:MorseKelley
    Wensheng Yu Tianyu Sun Yaoshun Fu Dakai Guo Si Chen et al.
    1.0.0
    LGPL-2.1
    Used by 0 other packages
    24 Jul 2024
  18. coq-msets-extra

    No documentation

    Extensions of MSets for Efficient Execution
    keyword:finite sets keyword:fold with abort keyword:extracting efficient code keyword:data structures category:Computer Science/Data Types and Data Structures category:Miscellaneous/Extracted Programs/Data structures logpath:MSetsExtra date:2019-09-19
    FireEye Formal Methods Team <formal-methods@fireeye.com> Thomas Tuerk <thomas@tuerk-brechen.de>
    1.2.0
    LGPL-2.1-only
    Used by 0 other packages
    19 Sep 2019
  19. coq-num-analysis

    No documentation

    Numerical Analysis in Coq
    category:Mathematics/Real Calculus and Topology keyword:real analysis keyword:Lax-Milgram theorem keyword:Lebesgue integration keyword:Tonelli theorem keyword:Bochner integration logpath:Lebesgue logpath:LM date:2022-09-06
    Sylvie Boldo François Clément Vincent Martin Micaela Mayero Florian Faissole et al.
    1.0.0
    LGPL-3.0-or-later
    Used by 0 other packages
    06 Sep 2022
  20. coq-of-ocaml

    No documentation

    Compile a subset of OCaml to Coq
    date:2020-03-20 keyword:compilation keyword:OCaml logpath:OCaml
    Guillaume Claret
    2.1.0
    MIT
    Used by 0 other packages
    20 May 2020
  21. coq-ollibs

    No documentation

    OL libraries
    keyword:standard library keyword:list keyword:permutation keyword:decidable equality keyword:finite multisets category:Mathematics/Combinatorics and Graph Theory date:2024-09-16 logpath:OLlibs
    Olivier Laurent Christophe Lucas
    2.0.7
    LGPL-3.0-or-later
    Used by 0 other packages
    17 Sep 2024
  22. coq-operads

    No documentation

    A Coq library defining operads
    keyword:operad category:Mathematics/Algebra date:2023-08-28 logpath:Operads
    Zachary Flores Angelo Taranto Eric Bond Yakir Forman
    1.1.0
    Used by 0 other packages
    29 Aug 2023
  23. coq-orb-stab

    No documentation

    Finite orbit-stabilizer theorem
    keyword: orbit keyword: stabilizer keyword: inclusion-exclusion category: Mathematics/Algebra date: 2008-01-5
    Robert Kam <rkam2001@hotmail.com> [none]
    8.9.0
    GNU Lesser Public License
    Used by 0 other packages
    08 Dec 2019
  24. coq-ordinal

    No documentation

    Ordinal Numbers in Coq
    date:2025-08-03 category:Mathematics/Logic keyword:ordinal numbers keyword:set theory logpath:Ordinal
    Minki Cho <minki.cho@sf.snu.ac.kr>
    0.5.6
    MIT
    Used by 0 other packages
    12 Aug 2025
  25. coq-ott

    No documentation

    Auxiliary Coq library for Ott, a tool for writing definitions of programming languages and calculi
    category:Computer Science/Semantics and Compilation/Semantics keyword:abstract syntax logpath:Ott date:2024-12-30
    Peter Sewell Francesco Zappa Nardelli Scott Owens
    0.34
    BSD-3-Clause
    Used by 1 other packages
    30 Dec 2024
  26. coq-paco

    No documentation

    Coq library implementing parameterized coinduction
    date:2025-01-30 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Mathematics/Logic keyword:co-induction keyword:simulation keyword:parameterized greatest fixed point logpath:Paco
    Chung-Kil Hur <gil.hur@sf.snu.ac.kr> Georg Neis <neis@mpi-sws.org> Derek Dreyer <dreyer@mpi-sws.org> Viktor Vafeiadis <viktor@mpi-sws.org> Minki Cho <minki.cho@sf.snu.ac.kr>
    4.2.3
    BSD-3-Clause
    Used by 4 other packages
    31 Jan 2025
  27. coq-param-pi

    No documentation

    Coding of a typed monadic pi-calculus using parameters for free names
    keyword: Pi-Calculus category: Computer Science/Lambda Calculi date: 1998-09-30
    Loïc Henry-Gréard
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  28. coq-paramcoq

    No documentation

    Plugin for generating parametricity statements to perform refinement proofs
    keyword:paramcoq keyword:parametricity keyword:OCaml modules category:Miscellaneous/Rocq Extensions logpath:Param date:2024-06-29
    Chantal Keller (Inria, École polytechnique) Marc Lasson (ÉNS de Lyon) Abhishek Anand Pierre Roux Emilio Jesús Gallego Arias et al.
    1.1.3+rocq9.0
    MIT
    Used by 4 other packages
    26 Mar 2025
  29. coq-parseque

    No documentation

    Total parser combinators in Coq
    category:Computer Science/Data Types and Data Structures date:2024-03-10 logpath:parseque
    G. Allais
    0.2.2
    MIT
    Used by 1 other packages
    10 Mar 2025
  30. coq-pi-agm

    No documentation

    Computing thousands or millions of digits of PI with arithmetic-geometric means
    keyword:real analysis keyword:pi category:Mathematics/Real Calculus and Topology logpath:agm date:2020-06-23
    Yves Bertot <yves.bertot@inria.fr>
    1.2.8
    CECILL-B
    Used by 0 other packages
    20 Jun 2024
  31. coq-pi-calc

    No documentation

    Pi-calculus in Coq
    keyword: process algebras keyword: pi-calculus keyword: concurrency keyword: higher-order syntax category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems date: 1998-07
    Ivan Scagnetto <scagnett@dimi.uniud.it>
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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
  50. 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
... 3 4 5 6