jfehrle Goto Github PK

aac-tactics

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

ceps

Coq Enhancement Proposals

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-elpi

Coq plugin embedding elpi

coq-equations

A function definition package for Coq

coq-ext-lib

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

coq-serapi

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

coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

coqtail

Interactive Coq Proofs in Vim

fiat-crypto

Cryptographic Primitive Code Generation by Fiat

metacoq

Metaprogramming in Coq

mtac2

ocaml

The core OCaml system: compilers, runtime system, base libraries

pg

This repo is the new home of Proof General

platform

Multi platform setup for Coq, Coq libraries and tools

relation-algebra

Relation algebra library for Coq

rewriter

Reflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting

structtact

Coq utility and tactic library.

verdi

A framework for formally verifying distributed systems implementations in Coq

verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

www

Source files of the coq.inria.fr website (static part)