skyskimmer Goto Github PK

.emacs.d

Emacs configuration

aac-tactics

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

adventofcode

analysis

Mathematical Components compliant Analysis Library

andromeda

A minimalist implementation of type theory, suitable for experimentation

argosy

Proving crash safety for systems with layered recovery

atbr

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

autoinduct

Taking a fun tactic implemented in class, and making it public for further refinement

autosubst-ocaml

bbv

Bedrock Bit Vector Library

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

category-theory

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

ceps

Coq Enhancement Proposals

certigraph

A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.

coinduction

coinduction library for Coq

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

A plugin for Coq that implements the call-by-name forcing translation

coq-lean-import

coq-library-undecidability

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

coq-lsp

Language Server Protocol for Coq

coq-ltac2-compiler

coq-plugin-lib

Library of useful utility functions for Coq plugins