In proof assistants, there is in general a clear separation between the
kernel of the system, the proof checker (hopefully sound, complete and
decidable), and its interface, all the (possibly unsound, incomplete,
semi-decidable) tools that allows the user to build a proof that, in the
end, is sent to the proof checker for verification. The interface and
the kernel do not need to use exactly the same language, but the
user-defined type system and theory need to be translatable into the
One possible approach to such an architecture, that can accommodate
different user-defined type systems/theories, is natural deduction or
type theory modulo some congruence on terms and propositions/types
generated by some set of user-defined rewrite rules [1,7,...]
(generalizing usual beta and iota reductions). For instance, considering
first-order logic and natural deduction modulo, by using appropriate
sets of rewrite rules, one can encode higher-order logic , Peano
arithmetic , Zermelo set theory , etc. In lambda-pi modulo (pure
type system with simple and term-dependent types only), one can encode
any functional pure type system including an arbitrary number of
universes  (but the case of pure type systems with subtyping has not
been studied yet). The use of type-level rewriting is essential for
these encodings to work.
Mathieu Boespflug developed a type-checker for lambda-pi modulo called
Dedukti . But it is just a type-checker: there is currently no
interface. Some works have been done for translating Coq  or
HOL-light proofs  into lambda-pi modulo.
Hope this can help,
 G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal
of Automated Reasoning, 31, 2003, pp. 33-72.
 G. Dowek, Th. Hardin, and C. Kirchner, HOL-lambda-sigma: an
intentional first-order expression of higher-order logic, Mathematical
Structures in Computer Science, 11, 2001, pp. 1-25.
 G. Dowek and A. Miquel, Cut elimination for Zermelo set theory
 G. Dowek and B. Werner, Arithmetic as a theory modulo, in J. Giesel
(Ed.), Term rewriting and applications, Lecture Notes in Computer
Science 3467, Springer-Verlag, 2005, pp. 423-437.
 D. Cousineau and G. Dowek, Embedding Pure Type Systems in the
lambda-Pi-calculus modulo, in S. Ronchi Della Rocca, Typed lambda
calculi and applications, Lecture Notes in Computer Science 4583,
Springer-Verlag, 2007, pp. 102-117.
 F. Blanqui. Definitions by rewriting in the Calculus of
Constructions. Mathematical Structures in Computer Science 15(1), p.
Le 08/06/2012 05:48, Michael Shulman a �crit :