Dedukti is a Logical Framework based on the $\lambda$$\Pi$-Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simple type theory, programming languages, Pure type systems, the Calculus of inductive constructions with universes, etc. and that permits to used it to check large libraries of proofs developed in other proof systems: Zenon, iProver, FoCaLiZe, HOL Light, and Matita.

翻译：Dedukti是一个基于$\lambda$$\Pi$-演算模理论的逻辑框架。我们证明，许多理论都可以在Dedukti中表达：构造性和经典谓词逻辑、简单类型理论、编程语言、纯类型系统、带宇宙的归纳构造演算等，并且这使得它能够用于检查在其他证明系统中开发的大型证明库：Zenon、iProver、FoCaLiZe、HOL Light和Matita。