Type-checking tools
- Dedukti: type-checker for the λΠ-calculus modulo rewriting
Proof development tools
- Lambdapi: proof assistant for the λΠ-calculus modulo rewriting, compatible with Dedukti
Proof translation tools
- Hol2dk: HOL-Light to Dedukti and Lambdapi translator
- CoqInE: Rocq to Dedukti translator
- Isabelle_Dedukti: Isabelle to Dedukti and Lambdapi translator
- Krajono: Matita to Dedukti translator
- Agda2Dedukti: Agda to Dedukti translator
- Lambdapi: Dedukti or Lambdapi to Rocq and Lean translator
- STTfaxport: tool to translate Dedukti proofs in the STTfa theory to Rocq, Lean3, PVS and OpenTheory
- Lrat2dk: LRAT to Dedukti translator
Proof libraries
- Coq-hol-light: translation of HOL-Light Multivariate library to Rocq
- Rocq-hollight-logic: translation of HOL-Light Logic library to Rocq
- Lambdapi-stdlib: Lambdapi standard library
- Logipedia: website providing a library of arithmetic proofs in Dedukti, Rocq, Lean, PVS and OpenTheory
- CoLoR: Coq library on rewriting theory and termination
Automated theorem proving tools
- ZenonModulo: extension of Zenon to deduction modulo generating Dedukti and Lambdapi proofs
- iProverModulo: extension of iProver with polarized resolution modulo
- ArchSAT: SMT/McSat solver producing Dedukti proofs
Other tools
- SizeChangeTool: termination checker for Dedukti