- Lambdapi: a
proof assistant for the λΠ-calculus modulo rewriting
- CoLoR: a Coq library on
rewriting theory and termination
- HOT: an automated termination prover for
- Moca: a generator of
construction functions for data types with algebraic relations on
- Rainbow: a
termination certificate verifier
a toolkit for generating and certifying processor simulators
Last updated on 13 October 2021.
Come back to main page.