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

A Learning Environment for Theorem Proving

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

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]

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

Proving crash safety for systems with layered recovery

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

A Coq tactic for proving multivariate inequalities using SDP solvers

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

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

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

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

TACACS protocol implemented in OCaml and Coq prover

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]