M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Certified Programs and Proofs -First International Conference, vol.7086, pp.135-150, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00639130

A. Assaf, A Framework for Defining Computational Higher-Order Logics, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01235303

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

A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek et al., Expressing Theories in the ??-Calculus Modulo Theory and in the Dedukti System, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01441751

A. Assaf and R. Cauderlier, Mixing HOL and Coq in Dedukti, 4th Workshop on Proof eXchange for Theorem Proving, vol.186, pp.89-96, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01141789

J. C. Blanchette, L. Bulwahn, and T. Nipkow, Automatic Proof and Disproof in Isabelle/HOL, Frontiers of Combining Systems, 8th International Symposium, vol.6989, pp.12-27, 2011.

G. Burel, Experimenting with Deduction Modulo, vol.6803, pp.162-176, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01125858

G. Bury, D. Delahaye, D. Doligez, P. Halmagrand, and O. Hermant, Automated Deduction in the B Set Theory using Typed Proof Search and Deduction Modulo, LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01204701

R. Cauderlier, A Rewrite System for Proof Constructivization, Proceedings of the 2016 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, vol.2, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01420634

R. Cauderlier and C. Dubois, ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti, Theoretical Aspects of Computing -ICTAC 2016 -13th International Colloquium, vol.9965, pp.459-468, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01420638

R. Cauderlier and P. Halmagrand, Checking Zenon Modulo Proofs in Dedukti, Proceedings 4th Workshop on Proof eXchange for Theorem Proving, vol.186, pp.57-73, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01171360

E. Denney, A Prototype Proof Translator from HOL to Coq, Theorem Proving in Higher Order Logics, 13th International Conference, vol.1869, pp.108-125, 2000.

T. Gauthier and C. Kaliszyk, Matching concepts across HOL libraries, Intelligent Computer Mathematics -International Conference, CICM 2014, Coimbra, Portugal, vol.8543, pp.267-281, 2014.

F. Horozal and F. Rabe, Representing Model Theory in a Type-Theoretical Logical Framework, Theoretical Computer Science, vol.412, pp.4919-4945, 2011.

D. J. Howe, Importing Mathematics from HOL into Nuprl, Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, vol.1125, pp.267-281, 1996.

B. Huffman and O. Kuncar, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Certified Programs and Proofs -Third International Conference, vol.8307, pp.131-146, 2013.

J. G. Hurd-;-m, K. Bobaru, G. J. Havelund, R. Holzmann, and . Joshi, The OpenTheory Standard Theory Library, NASA Formal MethodsThird International Symposium, NFM 2011, vol.6617, pp.177-191, 2011.

C. Kaliszyk and A. Krauss, Scalable LCF-Style Proof Translation, Interactive Theorem Proving, number 7998 in LNCS, pp.51-66, 2013.

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

D. Miller, Foundational Proof Certificates: Making Proof Universal and Permanent, Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, LFMTP 2013, pp.1-2, 2013.

F. Pessaux, FoCaLiZe: Inside an F-IDE, Proceedings 1st Workshop on Formal Integrated Development Environment, vol.149, pp.64-78, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01203501

V. Prevosto and M. Jaume, Making proofs in a hierarchy of mathematical structures, Proceedings of Calculemus, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01531083

R. Saillard, Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice, MINES Paritech, 2015.

C. Schürmann and M. Stehr, An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf, Logic for Programming, Artificial Intelligence, and Reasoning, number 4246 in LNCS, pp.150-166, 2006.

F. Wiedijk, Encoding the HOL Light logic in Coq, 2007.

T. Zimmermann and H. Herbelin, Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01152588