skyskimmer Goto Github PK

perennial

Verifying concurrent crash-safe systems

plugin_tutorials

A collection of small projects to illustrate how to write plugins for Coq

polygraph

Notes on ENS Lyon Polynomials and Graphs M2 course (2013-2014)

proofgeneral

This repo is a fork of Proof General

quickchick

Randomized Property-Based Testing Plugin for Coq

reduction-effects

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

relation-algebra

Relation algebra library for Coq

rewriter

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

rupicola

Extracting imperative code from Gallina

sf

stdpp

straight.el

🍀 Next-generation, purely functional package manager for the Emacs hacker.

tlc

Library for Classical Coq

topology

Formal topology (and some probability) in Coq

tuareg

Emacs OCaml mode

unicoq

An enhanced unification algorithm for Coq

unimath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

unit-test-test

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

vscoq

A Visual Studio Code extension for Coq [maintainers=@maximedenes,@fakusb]

vst

Verified Software Toolchain

zf

Playing around with axiomatic set theory in Coq