CoqInE

CoqInE is a translator of Coq proofs into Dedukti, a universal proof checker based on the lambda-Pi-calculus modulo formalism.

Although CoqInE has not been officially released yet, the source code of a preliminary version can be obtained via github.