A. Assaf and G. Burel, Translating HOL to Dedukti, Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, pp.74-88, 2015.
DOI : 10.4204/EPTCS.186.8
URL : https://hal.archives-ouvertes.fr/hal-01097412

A. Assaf and R. Cauderlier, Mixing HOL and Coq in Dedukti (Extended Abstract), Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, pp.89-96, 2015.
DOI : 10.4204/EPTCS.186.9

D. Cousineau and G. Dowek, Embedding pure type systems in the lambda-picalculus modulo, Typed lambda calculi and applications, pp.102-117, 2007.

M. William and . Farmer, The seven virtues of simple type theory, Journal of Applied Logic, vol.6, issue.3, pp.267-286, 2008.

T. Gauthier and C. Kaliszyk, Matching Concepts across HOL Libraries, Proc. of the 7th Conference on Intelligent Computer Mathematics (CICM'14), pp.267-281, 2014.
DOI : 10.1007/978-3-319-08434-3_20
URL : http://arxiv.org/abs/1405.3906

T. Gauthier and C. Kaliszyk, Matching Concepts across HOL Libraries, Intelligent Computer Mathematics, pp.267-281, 2014.
DOI : 10.1007/978-3-319-08434-3_20
URL : http://arxiv.org/abs/1405.3906

T. Gauthier and C. Kaliszyk, Sharing HOL4 and HOL Light Proof Knowledge, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15), p.2015
DOI : 10.1007/978-3-662-48899-7_26

J. Harrison, HOL Light: An Overview, Theorem Proving in Higher Order Logics, pp.60-66, 2009.
DOI : 10.1016/0304-3975(93)90095-B

J. Hurd, The OpenTheory Standard Theory Library, pp.177-191
DOI : 10.1007/3-540-60275-5_76

C. Kaliszyk and A. Krauss, Scalable LCF-Style Proof Translation, Interactive Theorem Proving, pp.51-66, 2013.
DOI : 10.1007/978-3-642-39634-2_7

M. Oliveira, A. Cavalcanti, and J. Woodcock, Unifying theories in proofpower-z, Unifying Theories of Programming, pp.123-140, 2006.

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

K. Slind and M. Norrish, A Brief Overview of HOL4, Theorem Proving in Higher Order Logics, pp.28-32, 2008.
DOI : 10.1007/s00165-007-0028-5

M. Wenzel, Interactive theorem provers from the perspective of isabelle/isar