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