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).

Coq formalization of guarded iteration a la https://www8.cs.fau.de/_media/research:papers:elgot-retract.pdf.

A Coq formalization of "Negative Translations and Normal Modality".

BSc project of Alexander Dietsch for simulating LOOP and WHILE programs

An abortive attempt by Ulrich R. to formalize de Groote's paper