- hol2dk: new
translator from HOL-Light to Dedukti and Lambdapi
- 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 24 March 2023.
Come back to main page.