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

Verified hash-based AMQ structures in Coq

A formalization of category theory in the Coq proof assistant.

Formalization of C++ for verification purposes.

A Lustre compiler in Coq

LVC verified compiler

A foundational framework for modular cryptographic proofs in Coq

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization

This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.

A verified polyhedral scheduling validator in Coq.

Verimag Polyhedra Library

A fornalisation of Grobner basis in ssreflect

Formalising Turing Machines In Coq (bachelor's thesis)

A library of formalized automaton algorithms

A Coq formalisation of the R programming language

les problèmes proposés par le journal Le Monde en Coq

Paper: Formalizing line editors in Coq

Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory