A framework for formally verifying distributed systems implementations in Coq

Replib: generic programming & Unbound: generic treatment of binders

A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]

Logical Relation for MLTT in Coq

The Coq formalization of the paper Reasoning about the garden of forking paths.

A Model of Relationally Parametric System F in Coq

The well-foundedness of the multiset ordering