A. Assaf, A calculus of constructions with explicit subtyping, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01097401

A. Assaf and G. Burel, Translating HOL to Dedukti. Draft, available at https, 2014.
DOI : 10.4204/eptcs.186.8
URL : https://hal.archives-ouvertes.fr/hal-01097412

M. Boespflug and G. Burel, CoqInE: Translating the calculus of inductive constructions into the ??-calculus modulo, PxTP, p.44, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126128

G. Burel, A shallow embedding of resolution and superposition proofs into the ??-calculus modulo, PxTP, pp.43-57, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01126321

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LPAR, number 8312 in LNCS, pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784

J. Hurd, The OpenTheory Standard Theory Library, NFM, number 6617 in LNCS, pp.177-191, 2011.
DOI : 10.1007/3-540-60275-5_76
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.474

C. Keller and B. Werner, Importing HOL Light into Coq, ITP, number 6172 in LNCS, pp.307-322, 2010.
DOI : 10.1007/978-3-642-14052-5_22
URL : https://hal.archives-ouvertes.fr/inria-00520604

R. Saillard, Dedukti: a universal proof checker, Foundation of Mathematics for Computer-Aided Formalization Workshop, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00833992

R. Saillard, Towards explicit rewrite rules in the ??-calculus modulo, IWIL -10th International Workshop on the Implementation of Logics, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00921340