Frédéric Blanqui

color. Coq library on rewriting theory and termination

moca. Generator of OCaml construction functions for quotient types

simsoc-cert. Generator of C code and Coq code for ISA and SoC

rainbow. Certified checker of CPF termination certificates

hot. Automated termination prover for higher-order rewriting