Dedukti is the implmentation of a logical framework based on a the dependent type theory LF augmented with higher-order rewrite rules. These rules are used in pratice to define a shallow embedding of some given source logic into Dedukti. Dedukti can then type-check proof objects of the source logic, and possibly move proof objects between different logics. This paradigm has already been applied to implementations of various proof logics, whether classical or intuitionistic, first-order or higher-order, including iProver, HOL Light, and Matita, this growing list is by no means exhaustive.

A particular application we are interested in is the encoding in Dedukti of the proof assistant Coq with its polymorphic universes.

The problem we address in this presentation is meta-theoretic: how to prove that a particular rewrite encoding yields a consistent rewrite theory. We illustrate this on-going work with rules for encoding polymnorphic universes.