Type-checking tools
- Dedukti: a type-checker for the λΠ-calculus modulo rewriting
Proof development tools
- Lambdapi: a proof assistant for the λΠ-calculus modulo rewriting, compatible with Dedukti
Proof translation tools
- CoqInE: a Coq to Dedukti translator
- Holide: an OpenTheory to Dedukti translator
- Agda2Dedukti: an Agda to Dedukti translator
- Isabelle_Dedukti: an Isabelle to Dedukti translator
- Krajono: a Matita to Dedukti translator
- Logipedia: a tool for translating Dedukti proofs in the theory STTfa to Coq, Lean, PVS and OpenTheory
- Ekstrakto: a TSTP to Dedukti translator
- SKonverto: generates a proof of a first-order formula from a proof of its skolemized version
- lrat2dk: a LRAT to Dedukti translator
Automated theorem proving tools
- ArchSAT: an SMT/McSat solver producing Dedukti proofs
- iProverModulo: an extension of iProver with polarized resolution modulo
- ZenonModulo: an extension of Zenon with rewriting generating Dedukti and Lambdapi proofs
Termination tools
- SizeChangeTool: a termination checker for Dedukti
Libraries
- Logipedia.science: a website providing a library of arithmetic proofs in Dedukti, Coq, Lean, PVS and OpenTheory
- Nubo: a repository of Dedukti proofs
- CoLoR: a Coq library on rewriting theory and termination
Code generation tools
- Moca: a generator of construction functions for data types with algebraic relations on constructors