Software
- hol2dk: proof
translator from HOL-Light to Dedukti and Lambdapi
- isabelle_dedukti:
proof translator from Isabelle 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
higher-order rewriting
- Moca: a generator of
construction functions for data types with algebraic relations on
constructors
- Rainbow: a
termination certificate verifier
- SimSoC-Cert:
a toolkit for generating and certifying processor simulators
Last updated on 2 October 2026.
Come back to main page.