A Coq library for Homotopy Type Theory

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

A Library for Representing Recursive and Impure Programs in Coq

Coq plugin embedding elpi

The mathematical study of type theories, in univalent foundations

Monadic effects and equational reasoning in Rocq

A (formalised) general definition of type theories

A Coq library for parametric coinduction

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

Ltac2 tutorial

Formalization of the polymorphic lambda calculus and its parametricity theorem

A Coq to Cedille compiler written in Coq

Tiny verified SAT-solver

a version of the 2048 game for Coq

A Model of Relationally Parametric System F in Coq

Mechanized Type Soundness Proofs using Definitional Interpreters

Formalisation of a coinductive confluence proof for the infinitary lambda calculus.

Cut elimination for the logic of Bunched Implications (BI), and some extensions.