The CompCert formally-verified C compiler

A Coq library for Homotopy Type Theory

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

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

Formal Reasoning About Programs

Mathematical Components

Tricks you wish the Coq manual told you [maintainer=@tchajed]

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

Convert Haskell source code to Coq source code

Randomized Property-Based Testing Plugin for Coq

FSCQ is a certified file system written and proven in Coq

A Library for Representing Recursive and Impure Programs in Coq

A function definition package for Coq

🐣 A blog engine written and proven in Coq

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

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

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

A formalisation of the Calculus of Constructions

Coq development for the course "Mechanized semantics", Collège de France, 2019-2020

A Specification for Dependent Types in Haskell (Core)

A (formalised) general definition of type theories

A Coq library for parametric coinduction

Total Parser Combinators in Coq [maintainer=@womeier]

A blog about Coq

Old Coq plugin for parametricity [maintainer=@ppedrot]

Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016

Graph Theory [maintainers=@chdoc,@damien-pous]

Companion Coq development for Xavier Leroy's 2021 lectures on program logics

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

A Coq library for abstract syntactical reasoning