D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, 8th International Conference Proceedings. Volume 4583 of Lecture Notes in Computer Science, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

J. M. Hurd, K. Havelund, G. J. Holzmann, and R. Joshi, The OpenTheory Standard Theory Library, Third International Symposium on NASA Formal Methods, pp.177-191, 2011.
DOI : 10.1007/3-540-60275-5_76

URL : http://www.gilith.com/research/papers/stdlib.pdf

G. Gonthier, Engineering mathematics: the odd order theorem proof, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pp.1-2, 2013.
DOI : 10.1145/2429069.2429071

R. Cauderlier and C. Dubois, FoCaLiZe and Dedukti to the Rescue for Proof Interoperability
DOI : 10.1007/11916277_11

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

R. Saillard, Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique), p.7, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01299180

T. Coquand, An analysis of girard's paradox, LICS, IEEE Computer Society, pp.227-236, 1986.

P. B. Andrews, An introduction to mathematical logic and type theory -to truth through proof. Computer science and applied mathematics, 1986.
DOI : 10.1007/978-94-015-9934-4