Utabcert is a Coq formalization of equivalence and containment results obtained by Sagiv and Yannakakis (Equivalence Among Relational Expressions with the Union and Difference Operators).
BSc project of Alexander Dietsch for simulating LOOP and WHILE programs
Paul Wild's development of Aarhus ModuRes library
A Coq formalization of "Negative Translations and Normal Modality".
BSc project of Michael Banken on simulating counter machines
An abortive attempt by Ulrich R. to formalize de Groote's paper