B. Peter and . Andrews, An introduction to mathematical logic and type theory-to truth through proof. Computer science and applied mathematics, 1986.

A. Asperti, W. Ricciotti, C. Sacerdoti-coen-&-enrico, and . Tassi, The Matita Interactive Theorem Prover, Automated Deduction-CADE-23-23rd International Conference on Automated Deduction, pp.64-69, 2011.

R. Cauderlier-&-catherine and . Dubois, FoCaLiZe and Dedukti to the Rescue for Proof Interoperability, Interactive Theorem Proving8th International Conference, pp.131-147, 2017.

Z. Chihani, D. Miller-&-fabien, and R. , Foundational Proof Certificates in First-Order Logic, Automated Deduction-CADE-24-24th International Conference on Automated Deduction, vol.7898, pp.162-177, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00906485

T. Coquand, An Analysis of Girard's Paradox, Proceedings of the Symposium on Logic in Computer Science (LICS '86), pp.227-236, 1986.

D. Cousineau-&-gilles and . Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, 8th International Conference, vol.4583, pp.102-117, 2007.

R. Harper, F. Honsell-&-gordon, and D. Plotkin, A Framework for Defining Logics, J. ACM, vol.40, issue.1, pp.143-184, 1993.

J. Hurd, The OpenTheory Standard Theory Library, Third International Symposium on NASA Formal Methods (NFM 2011), vol.6617, pp.177-191, 2011.

C. Keller-&-benjamin and . Werner, Importing HOL Light into Coq, Interactive Theorem Proving, First International Conference, vol.6172, pp.307-322, 2010.

F. Pfenning and &. C. Elliott, Higher-order Abstract Syntax, SIGPLAN Not, vol.23, issue.7, pp.199-208, 1988.

B. Pientka, A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, 35th Annual ACM Symposium on Principles of Programming Languages (POPL'08, pp.371-382, 2008.

R. Saillard, Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique), Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice, 2015.

, The Coq Proof Assistant, version 8.7.1. Available at, 2017.

, Arithmetic library, The Matita development team, 2018.

F. Thiré, Interoperability in Dedukti: From the Calculus of Inductive Constructions to an extension of HOL, 2018.

F. Thiré, Sharing a library between proof assistants: reaching out to the HOL family, 2018.