ppedrot Goto Github PK

aac-tactics

This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.

argosy

Proving crash safety for systems with layered recovery

atbr

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

bbv

Bedrock Bit Vector Library

bedrock

Not necessarily up-to-date mirror of hg bedrock repository

bedrock2

A work-in-progress language and compiler for verified low-level programming

bignums

Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library

bot

A (Coq Development Team) bot written in OCaml

camlp5

Preprocessor / Pretty Printer for OCaml

camlp5-engine

A standalone version of the camlp5 parsing engine

category-theory

An axiom-free formalization of category theory in Coq for personal study and practical work

ceps

Coq Enhancement Proposals

cheerios

Formally verified Coq serialization library with support for extraction to OCaml

color

Coq library on rewriting theory and termination

compcert

The CompCert formally-verified C compiler

coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

coq-array

Coq library for array indexing and subslicing

coq-bench

coq-dpdgraph

Build dependency graphs between COQ objects

coq-elpi

Coq plugin embedding elpi

coq-equations

A plugin for Coq to add dependent pattern-matching.

coq-ext-lib

A library of Coq definitions, theorems, and tactics.

coq-forcing

Tentative implementation of call-by-name forcing in Coq

coq-in-coq

A formalisation of the Calculus of Constructions

coq-lean-import

coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.

coq-lsp

Language Server Protocol and VS Code Extension for Coq

coq-performance-tests

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

coq-scripts

Various useful scripts for dealing with Coq files

coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.