## Type-checking tools

- Dedukti: a type-checker for the λΠ-calculus modulo rewriting

- Dedukti: a type-checker for the λΠ-calculus modulo rewriting

- Lambdapi: a proof assistant for the λΠ-calculus modulo rewriting, compatible with Dedukti

- 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

- 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

- SizeChangeTool: a termination checker for Dedukti

- 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

- Moca: a generator of construction functions for data types with algebraic relations on constructors