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

Mathematical Components

A Learning Environment for Theorem Proving with the Coq proof assistant

A library for formalizing Haskell types and functions in Coq

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

Formalising Type Theory in a modular way for translations between type theories

A web server written in Coq.

A Formalization of Typed and Untyped λ-Calculi in Coq and Agda2

A blog about Coq

Coq code accompanying several articles on semantics of functional programming languages

Pi-calculus in Coq

Control-flow based language verification framework