270 search results for "tag:"logpath:""

Showing 151 - 200
  1. coq-mathcomp-sum-of-two-square

    No documentation

    A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file :
    logpath:mathcomp.contrib.sum_of_two_square
    Laurent Thery
    1.0.1
    MIT
    Used by 0 other packages
    09 May 2018
  2. 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
  3. 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
  4. coq-mathcomp-zify

    No documentation

    Micromega tactics for Mathematical Components
    logpath:mathcomp.zify
    Kazuhiko Sakaguchi
    1.5.0+2.0+8.16
    CECILL-B
    Used by 5 other packages
    12 Jul 2023
  5. 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
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 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
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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
  23. coq-parsec

    No documentation

    Monadic parser combinator library in Coq
    category:Computer Science/Data Types and Data Structures keyword:string logpath:Parsec
    Yishuai Li <yishuai@cis.upenn.edu> Azzam Althagafi <aazzam@cis.upenn.edu> Yao Li <liyao@cis.upenn.edu> Li-yao Xia <xialiyao@cis.upenn.edu> Benjamin C. Pierce <bcpierce@cis.upenn.edu>
    0.2.0
    BSD-3-Clause
    Used by 2 other packages
    09 Oct 2024
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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
  32. 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
  33. 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
  34. 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
  35. 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
  36. 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
  37. 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
  38. 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
  39. 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
  40. 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
  41. 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
  42. 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
  43. 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
  44. 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
  45. 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
  46. 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
  47. 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
  48. 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
  49. 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
  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
... 3 4 5 6