487 search results for ""

Showing 301 - 350
  1. coq-metacoq-erasure

    No documentation

    Implementation and verification of an erasure procedure for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 5 other packages
    03 Apr 2025
  2. coq-metacoq-erasure-plugin

    No documentation

    Implementation and verification of an erasure procedure for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 2 other packages
    03 Apr 2025
  3. coq-metacoq-pcuic

    No documentation

    A type system equivalent to Coq's and its metatheory
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 6 other packages
    03 Apr 2025
  4. coq-metacoq-quotation

    No documentation

    Gallina quotation functions for Template Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 1 other packages
    03 Apr 2025
  5. coq-metacoq-safechecker

    No documentation

    Implementation and verification of safe conversion and typechecking algorithms for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 4 other packages
    03 Apr 2025
  6. coq-metacoq-safechecker-plugin

    No documentation

    Implementation and verification of an erasure procedure for Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 1 other packages
    03 Apr 2025
  7. coq-metacoq-template

    No documentation

    A quoting and unquoting library for Coq in Coq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 8 other packages
    03 Apr 2025
  8. coq-metacoq-template-pcuic

    No documentation

    Translations between Template Coq and PCUIC and proofs of correctness
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 6 other packages
    03 Apr 2025
  9. coq-metacoq-translations

    No documentation

    Translations built on top of MetaCoq
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 1 other packages
    03 Apr 2025
  10. coq-metacoq-utils

    No documentation

    The utility library of Template Coq and PCUIC
    Abhishek Anand <aa755@cs.cornell.edu> Danil Annenkov <danil.v.annenkov@gmail.com> Simon Boulier <simon.boulier@inria.fr> Cyril Cohen <cyril.cohen@inria.fr> Yannick Forster <forster@ps.uni-saarland.de> et al.
    1.3.4+9.0
    MIT
    Used by 3 other packages
    03 Apr 2025
  11. 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
  12. 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
  13. 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
  14. coq-minic

    No documentation

    Semantics of a subset of the C language
    keyword: denotational semantics keyword: compilation category: Computer Science/Semantics and Compilation/Semantics
    Eduardo Giménez and Emmanuel Ledinot
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  15. coq-miniml

    No documentation

    Correctness of the compilation of Mini-ML into the Categorical Abstract Machine
    keyword: functional programming keyword: Categorical Abstract Machine keyword: compilation keyword: natural semantics category: Computer Science/Semantics and Compilation/Compilation
    Samuel Boutin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  16. coq-mirror-core

    No documentation

    A framework for computational reflection
    Gregory Malecha
    1.0.2
    BSD
    Used by 0 other packages
    17 Jul 2016
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. coq-monae

    No documentation

    Monads and equational reasoning in Coq
    keyword:monae keyword:effects keyword:probability keyword:nondeterminism logpath:monae.theories logpath:monaeImpredicativeSet date: 2025-02-26
    Reynald Affeldt David Nowak Takafumi Saikawa Jacques Garrigue Ayumu Saito et al.
    0.9.0
    LGPL-2.1-or-later
    Used by 0 other packages
    26 Feb 2025
  23. 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
  24. 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
  25. coq-mtac

    No documentation

    Typed Tactics for Coq 8.5
    Beta Ziliani
    1.3.0
    MIT
    Used by 0 other packages
    24 May 2016
  26. coq-mtac2

    No documentation

    Typed tactic language for Coq
    Beta Ziliani <beta.ziliani@gmail.com> Jan-Oliver Kaiser <janno@mpi-sws.org Robbert Krebbers <mail@robbertkrebbers.nl> Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr>
    1.4+8.20
    MIT
    Used by 0 other packages
    22 Nov 2024
  27. coq-multiplier

    No documentation

    Proof of a multiplier circuit
    keyword: hardware verification keyword: circuit category: Computer Science/Architecture category: Miscellaneous/Extracted Programs/Hardware
    Christine Paulin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  28. coq-mutual-exclusion

    No documentation

    A certification of Peterson's algorithm for managing mutual exclusion
    keyword: mutual exclusion keyword: concurrency keyword: Peterson's algorithm keyword: co-inductive types keyword: co-induction category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols category: Miscellaneous/Extracted Programs/Automata and protocols
    Eduardo Giménez
    8.9.0
    LGPL 2.1
    Used by 0 other packages
    08 Dec 2019
  29. coq-nfix

    No documentation

    Nfix: a Coq extension for fixpoints on nested inductives
    keyword: mutual fixpoint functions category: Miscellaneous/Coq Extensions
    Stéphane Lescuyer
    8.10.0
    Unknown
    Used by 0 other packages
    19 Oct 2020
  30. 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
  31. 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
  32. 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
  33. coq-opam-website

    No documentation

    Generation of a Coq website for OPAM: http://coq.io/opam/
    Guillaume Claret
    1.4.0
    MIT
    Used by 0 other packages
    26 Nov 2015
  34. 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
  35. 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
  36. coq-ordinal

    No documentation

    Ordinal Numbers in Coq
    date:2025-03-25 category:Mathematics/Logic keyword:ordinal numbers keyword:set theory logpath:Ordinal
    Minki Cho <minki.cho@sf.snu.ac.kr>
    0.5.5
    MIT
    Used by 0 other packages
    25 Mar 2025
  37. 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
  38. coq-otway-rees

    No documentation

    Otway-Rees cryptographic protocol
    keyword: Otway-Rees keyword: protocols keyword: cryptography category: Computer Science/Concurrent Systems and Protocols/Correctness of specific protocols
    Dominique Bolignano and Valérie Ménissier-Morain
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  39. 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
  40. coq-paradoxes

    No documentation

    Paradoxes in Set Theory and Type Theory
    keyword: Reynolds paradox keyword: Burali-Forti paradox keyword: Diaconescu paradox keyword: set theory keyword: system U keyword: inconsistency keyword: Hurkens paradox category: Mathematics/Logic/Foundations
    Bruno Barras Thierry Coquand Hugo Herbelin Benjamin Werner
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  41. 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
  42. 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
  43. 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
  44. 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
  45. coq-pautomata

    No documentation

    Parameterized automata
    keyword: p-automata keyword: ABR keyword: PGM keyword: time category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems
    Emmanuel Freund & Christine Paulin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  46. coq-persistent-union-find

    No documentation

    Persistent Union Find
    keyword: program verification keyword: union-find keyword: data structures keyword: Tarjan category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms
    Jean-Christophe Filliâtre
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  47. 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
  48. 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
  49. 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
  50. 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
... 6 7 8 ... 10