A. Assaf and G. Burel, Translating HOL to Dedukti, Electronic Proceedings in Theoretical Computer Science, vol.186, 2013.
DOI : 10.4204/EPTCS.186.8
URL : https://hal.archives-ouvertes.fr/hal-01097412

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.1-31, 1994.
DOI : 10.1093/logcom/4.3.217

J. Christian-blanchette, S. Bhme, and L. C. Paulson, Extending Sledgehammer with SMT solvers, Nikolaj Bjørner and Viorica Sofronie-Stokkermans, pp.116-130, 2011.

M. Boespflug and G. Burel, CoqInE: Translating the calculus of inductive constructions into the ??-calculus modulo, Second International Workshop on Proof Exchange for Theorem Proving, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126128

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, Second International Workshop on Proof Exchange for Theorem Proving, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

G. Burel, Experimenting with Deduction Modulo, Nikolaj Bjørner and Viorica Sofronie- Stokkermans, pp.162-176, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, LNCS, vol.4583, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9
URL : http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/Partage/tlca07.pdf

A. Dorra, ´ Equivalence de Curry-Howard entre le lambda-Pi-calcul et la logique intuitionniste, 2011.

G. Dowek, Polarized Resolution Modulo, IFIP TCS, pp.182-196, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460

H. Jean and . Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, volume 5 of Computer Science and Technology Series, 1986.

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
URL : http://www.cs.cmu.edu/~rwh/papers/lf/jacm93.ps

G. Klein, seL4, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.
DOI : 10.1145/1743546.1743574

K. Korovin, iProver ??? An Instantiation-Based Theorem Prover for First-Order Logic (System Description), LNAI, vol.5195, pp.292-298, 2008.
DOI : 10.1007/978-3-540-71070-7_24

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

F. Pfenning, Structural Cut Elimination, Information and Computation, vol.157, issue.1-2, pp.84-141, 2000.
DOI : 10.1006/inco.1999.2832

A. Riazanov and A. Voronkov, Vampire 1.1, Automated Reasoning, pp.376-380, 2001.
DOI : 10.1007/3-540-45744-5_29

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

S. Schultz, System description: E 0.81, LNCS, vol.3097, pp.223-228, 2004.

G. Sutcliffe, The TPTP World ??? Infrastructure for Automated Reasoning, LPAR, number 6355 in LNAI, pp.1-12, 2010.
DOI : 10.1007/978-3-642-17511-4_1

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS Version 3.5, LNCS, vol.18, issue.2-4, pp.140-145, 2009.
DOI : 10.1007/978-3-540-73595-3_38