Discover coq-community/coq-plugin-template Open Source project

Stars
17
Rank 1,257,181 (Top 25 %)
Language
OCaml
License
Other
Created about 6 years ago
Updated over 1 year ago

coq-community

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Template project for Coq plugins using the Dune build system, showcasing some advanced features [maintainer=@ejgallego]

coq-tricks

Tricks you wish the Coq manual told you [maintainer=@tchajed]

Coq

497

vscoq

A Visual Studio Code extension for Coq [maintainers=@rtetley,@huynhtrankhanh,@thery,@Blaisorblade]

OCaml

333

awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

304

math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

Coq

160

fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

Coq

158

coq-ext-lib

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

Coq

126

corn

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

Coq

108

coq-art

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

Coq

107

coq-dpdgraph

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

Coq

manifesto

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

coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

Coq

hydra-battles

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Coq

coq-100-theorems

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

HTML

autosubst

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

Coq

topology

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

Coq

semantics

A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]

Coq

fav-ssr

Functional Algorithms Verified in SSReflect [maintainer=@clayrat]

Coq

paramcoq

Coq plugin for parametricity [maintainer=@proux01]

Coq

dedekind-reals

A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]

Coq

parseque

Total Parser Combinators in Coq [maintainer=@womeier]

Coq

reglang

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

Coq

docker-coq

Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]

Dockerfile

coqdocjs

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

JavaScript

coqffi

Automatically generates Coq FFI bindings to OCaml libraries [maintainer=@lthms]

OCaml

coq-nix-toolbox

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]

Nix

graph-theory

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

Coq

chapar

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

Coq

aac-tactics

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

OCaml

goedel

Archived since the contents have been moved to the Hydras & Co. repository

Coq

gaia

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

Coq

dblib

Coq library for working with de Bruijn indices [maintainer=@KevOrr]

Coq

coq-program-verification-template

Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]

Coq

lemma-overloading

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

Coq

alea

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

Coq

atbr

Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]

Coq

bits

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

Coq

bignums

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Coq

coqoban

Sokoban (in Coq) [maintainer=@erikmd]

Coq

sudoku

A certified Sudoku solver in Coq [maintainers=@siraben,@thery]

Coq

HighSchoolGeometry

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

Coq

apery

A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]

Coq

hoare-tut

A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]

Coq

trocq

A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]

Coq

metaprogramming-rosetta-stone

A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]

Coq

coqtail-math

Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis. [maintainer=@jmadiot]

Coq

huffman

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

Coq

templates

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

Mustache

tarjan

Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]

Coq

regexp-Brzozowski

Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

Coq

qarith-stern-brocot

Binary rational numbers in Coq [maintainer=@herbelin]

Coq

docker-coq-action

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

Shell

mmaps

Modular Finite Maps over Ordered Types in Coq [maintainers=@letouzey,@palmskog]

Coq

notation-gallery

Examples showing best practices for using Coq notations and custom entries [maintainer=@bcpierce00]

Coq

comp-dec-modal

Completeness and Decidability of Modal Logic Calculi [maintainer=@chdoc]

Coq

buchberger

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

Coq

proviola

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

Python

coq-performance-tests

A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]

Coq

generic-environments

Coq library that provides an abstract data type for environments [maintainer=@aerabi]

Coq

zorns-lemma

Archived since the contents have been moved to the topology repository

Coq

reduction-effects

A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]

Makefile

docker-base

Parent image for Docker images of the Coq proof assistant [maintainers=@erikmd,@himito]

Dockerfile

almost-full

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

Coq

jmlcoq

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

Coq

bertrand

Coq proof of Bertrand's postulate on existence of primes [maintainer=@thery]

Coq

run-coq-bug-minimizer

Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]

Shell

pocklington

Pocklington's criterion for primality in Coq [maintainer=@Casteran]

Coq

vscoq-legacy

Legacy Visual Studio Code extension for Coq [maintainers=@huynhtrankhanh,@thery,@Blaisorblade]

TypeScript

stalmarck

Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]

Coq

exact-real-arithmetic

Exact Real Arithmetic [maintainers=@ybertot,@magaud]

Coq

coq-community/coq-plugin-template

coq-community

Reviews

Repository Details

More Repositories