coq-community

Repositories

• coq-performance-tests

  A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]
  Coq MIT 0 3 0 0 Updated Jul 8, 2020

• corn

  Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

  coq coq-library real-number
  Coq GPL-2.0 34 90 6 (2 issues need help) 2 Updated Jul 7, 2020

• docker-base

  Parent image for Docker images of the Coq proof assistant [maintainer=@erikmd]

  docker-coq
  Dockerfile BSD-3-Clause 0 3 0 1 Updated Jul 7, 2020

• docker-coq

  Docker images of the Coq proof assistant [maintainer=@erikmd]

  dockerfile ci docker-image coq opam docker-coq
  Dockerfile BSD-3-Clause 3 20 1 2 Updated Jul 7, 2020

• HighSchoolGeometry

  Geometry in Coq for French high school [maintainer=@thery]

  geometry coq high-school
  Coq LGPL-2.1 0 6 1 0 Updated Jul 6, 2020

• huffman

  Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]

  ocaml coq huffman-coding huffman-tree coq-extraction
  Coq 3 10 0 0 Updated Jul 6, 2020

• templates

  Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@palmskog,@Zimmi48]

  continuous-integration coq mustache-templates
  HTML Unlicense 4 5 15 2 Updated Jul 6, 2020

• graph-theory

  Graph Theory [maintainers=@chdoc,@damien-pous]

  coq graph-theory mathcomp
  Coq 1 3 0 0 Updated Jul 3, 2020

• paramcoq

  Coq plugin for parametricity [maintainer=@proux01]

  coq coq-plugin parametricity
  Coq 18 31 1 1 Updated Jul 3, 2020

• docker-coq-action

  GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]

  continuous-integration coq actions opam action docker-coq container-ci
  Shell MIT 2 3 3 (2 issues need help) 0 Updated Jun 30, 2020

• aac-tactics

  Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainers=@fakusb,@palmskog]

  coq coq-plugin coq-tactic
  OCaml 13 16 2 0 Updated Jun 29, 2020

• coqoban

  Sokoban (in Coq) [maintainer=@erikmd]

  puzzle coq coq-library
  Coq LGPL-2.1 2 4 0 0 Updated Jun 25, 2020

• reglang

  Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]

  regexp coq regular-languages ssreflect mathcomp
  Coq 2 16 2 0 Updated Jun 23, 2020

• almost-full

  Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=@palmskog]

  coq termination ramsey
  Coq MIT 0 0 0 0 Updated Jun 23, 2020

• vscoq

  A Visual Studio Code extension for Coq [maintainer=@maximedenes]

  editor coq vscode vscode-extension
  TypeScript MIT 20 103 32 6 Updated Jun 22, 2020

• manifesto

  Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.

  coq manifesto community-driven
  6 52 29 0 Updated Jun 20, 2020

• jmlcoq

  Coq definition of JML and a verified runtime assertion checker [maintainer=@palmskog]

  java coq jml runtime-checking
  Coq MIT 0 0 0 0 Updated Jun 12, 2020

• lemma-overloading

  Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]

  automation coq typeclasses ssreflect paper-artifacts canonical-structures mathcomp
  Coq GPL-3.0 7 17 0 0 Updated Jun 10, 2020

• proviola

  Tool for reanimation of Coq proofs [maintainer=@JasonGross]

  css html xml coq xsl coqdoc
  Python GPL-3.0 0 3 12 0 Updated Jun 7, 2020

• stalmarck

  A proof of Stålmarck's algorithm in Coq [maintainer=@palmskog]

  algorithm coq formalization coq-plugin coq-extraction
  Coq LGPL-2.1 1 1 0 0 Updated Jun 7, 2020

• coq-ext-lib

  A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

  library programming coq
  Coq 29 91 11 1 Updated Jun 6, 2020

• semantics

  A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
  Coq MIT 2 16 0 0 Updated Jun 5, 2020

• hoare-tut

  A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
  Coq LGPL-3.0 0 6 0 0 Updated Jun 5, 2020

• qarith-stern-brocot

  Binary Rational Numbers [maintainer=@herbelin]

  coq coq-library paper-artifacts
  Coq LGPL-2.1 2 1 0 1 Updated Jun 2, 2020

• awesome-coq

  A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]

  awesome coq resources awesome-list
  CC0-1.0 3 64 4 1 Updated May 31, 2020

• coq-art

  Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

  coq exercises coq-art
  Coq 6 23 1 0 Updated May 31, 2020

• buchberger

  Verified implementation of Buchberger's algorithm for computing Gröbner bases in Coq [maintainer=@palmskog]

  coq grobner-basis coq-extraction buchberger-algorithm
  Coq LGPL-2.1 1 1 0 0 Updated May 31, 2020

• alea

  Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]

  coq probability monad randomized-algorithms
  Coq LGPL-2.1 0 3 2 0 Updated May 29, 2020

• bits

  A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]

  coq coq-library ssreflect paper-artifacts coq-extraction
  Coq Apache-2.0 2 6 0 0 Updated May 29, 2020

• chapar

  A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

  distributed-systems key-value ocaml coq proof causal-consistency coq-extraction
  Coq MIT 6 26 3 0 Updated May 29, 2020