A Learning Environment for Theorem Proving

Lecture notes for a short course on proving/programming in Coq via SSReflect.

Proving crash safety for systems with layered recovery

CoqTL allows users to write model transformations and prove engine/transformation correctness in Coq

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

Lens, State is your father... and I can prove It!

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

PolyGen is a code generator for the polyhedral model, written and proved in Coq.

A Coq tactic for proving multivariate inequalities using SDP solvers

Attempt to prove semantic preservation (forward simulation) for a simple compiler.

TACACS protocol implemented in OCaml and Coq prover

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 development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=@palmskog]

Demo of using Iris to prove a simple property of a concurrent program

Project in Programming Language Seminar. Implement and prove properties about finger trees.

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