Software
- 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
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 24 March 2023.
Come back to main page.