Coq formalization of QRC1
2020-now
A Coq implementation of the Quantified Reflection Calculus with one modality.

templates
2021
Templates for configuration and other boilerplate files for Coq projects hosted on Gitlab, adapted from coq-community’s templates project.

Formalization of Basic Concepts from Tree Automata Theory in Coq
2020

Worms in Coq
2018
A Coq implementation of the Worm Calculus, the (closed fragment of the) Reflection Calculus, and the relationship between them.