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

A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

Formal Reasoning About Programs

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

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

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

A framework for smart contract verification in Coq

Modeling and Proving in Computational Type Theory

A quantum circuit language and formal verification tool

A Small Quantum Intermediate Representation

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Functional Data Structures and Algorithms in SSReflect [maintainer=@clayrat]

Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]

Coq library for reasoning about quantum programs

Coq course at Chalmers CSE

Coq code accompanying several articles on semantics of functional programming languages

Code and examples from the book 'Interactive Theorem Proving and Program Development' (Coq'Art book)

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]