G. Gonthier, A computer-checked proof of the Four Colour Theorem, unpublished, 2005.

B. Chetali, A world-first smart card CC certificate with formal assurances, presented at the Third Franco-Japanese Computer Security Workshop, 2008.

B. Chetali and Q. H. Nguyen, Industrial Use of Formal Methods for a High-Level Security Evaluation, FM, pp.198-213, 2008.
DOI : 10.1007/978-3-540-68237-0_15

G. Dowek, T. Hardin, and C. Kirchner, Theorem Proving Modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

G. Peterson and M. E. Stickel, Complete Sets of Reductions for Some Equational Theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981.
DOI : 10.1145/322248.322251

H. Barendregt and E. Barendsen, Autarkic Computations in Formal Proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002.
DOI : 10.1023/A:1015761529444

R. Bonichon, TaMeD: A Tableau Method for Deduction Modulo, IJCAR, pp.445-459, 2004.
DOI : 10.1007/978-3-540-25984-8_33

G. Burel, Unbounded Proof-Length Speed-Up in Deduction Modulo, CSL 2007, pp.496-511, 2007.
DOI : 10.1007/978-3-540-74915-8_37
URL : https://hal.archives-ouvertes.fr/inria-00138195

M. Crabbé, Non-normalisation de la théorie de Zermelo, manuscript, 1974.

R. Bonichon and O. Hermant, A Semantic Completeness Proof for TaMeD, LPAR, pp.167-181, 2006.
DOI : 10.1007/11916277_12
URL : https://hal.archives-ouvertes.fr/hal-01337086

O. Hermant, Méthodes Sémantiques en Déduction Modulo, 2005.

G. Dowek, Polarized resolution modulo, manuscript, 2009.
DOI : 10.1007/978-3-642-15240-5_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.154.5578

G. Dowek, Confluence as a Cut Elimination Property, RTA, pp.2-13, 2003.
DOI : 10.1007/3-540-44881-0_2

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

G. Dowek, What Is a Theory?, STACS, pp.50-64, 2002.
DOI : 10.1007/3-540-45841-7_3

N. Dershowitz and C. Kirchner, Abstract canonical presentations, Theoretical Computer Science, vol.357, issue.1-3, pp.53-69, 2006.
DOI : 10.1016/j.tcs.2006.03.012
URL : https://hal.archives-ouvertes.fr/inria-00121760

M. P. Bonacina and N. Dershowitz, Abstract canonical inference, ACM Transactions on Computational Logic, vol.8, issue.1
DOI : 10.1145/1182613.1182619
URL : http://arxiv.org/abs/cs/0406030

G. Burel and C. Kirchner, Completion Is an Instance of Abstract Canonical System Inference, Algebra, Meaning and Computation, pp.497-520, 2006.
DOI : 10.1007/11780274_26
URL : https://hal.archives-ouvertes.fr/inria-00000775

G. Burel and C. Kirchner, Cut Elimination in Deduction Modulo by Abstract Completion, LFCS, pp.115-131, 2007.
DOI : 10.1007/978-3-540-72734-7_9
URL : https://hal.archives-ouvertes.fr/inria-00115556

F. Baader and T. Nipkow, Term Rewriting and all That, 1998.

G. Gentzen, Untersuchungen ???ber das logische Schlie???en. I, Mathematische Zeitschrift, vol.39, issue.1, pp.176-210, 1934.
DOI : 10.1007/BF01201353

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

G. Dowek, About Folding-Unfolding Cuts and Cuts Modulo, Journal of Logic and Computation, vol.11, issue.3, pp.419-429, 2001.
DOI : 10.1093/logcom/11.3.419
URL : https://hal.archives-ouvertes.fr/inria-00072640

G. Burel, Automating Theories in Intuitionistic Logic, FroCoS, pp.181-197, 2009.
DOI : 10.1016/0168-0072(95)00005-2
URL : https://hal.archives-ouvertes.fr/inria-00395934

O. Hermant, A Model-based Cut Elimination Proof, in: 2nd St-Petersburg Days of Logic and Computability, 2003.

J. Endrullis, H. Geuvers, and H. Zantema, Degrees of Undecidability in Term Rewriting, CSL, pp.255-270, 2009.
DOI : 10.1007/978-3-540-70590-1_30

N. Dershowitz and C. Kirchner, Abstract saturation-based inference, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.65-74, 2003.
DOI : 10.1109/LICS.2003.1210046
URL : https://hal.archives-ouvertes.fr/inria-00099466

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

J. Girard, Y. Lafont, and P. Taylor, of Cambridge Tracts in Theoretical Computer Science, Proofs and Types, 1989.

O. Hermant, Semantic Cut Elimination in the Intuitionistic Sequent Calculus, TLCA, pp.221-233, 2005.
DOI : 10.1007/11417170_17

G. Dowek and B. Werner, Abstract, The Journal of Symbolic Logic, vol.87, issue.04, pp.1289-1316, 2003.
DOI : 10.1007/BFb0037116

M. Aiguier, C. Boin, and D. Longuet, On Generalized Theorems for Normalization of Proofs, Tech. Rep., LaMI -CNRS and, 2005.

M. Fitting, First-order logic and automated theorem proving, 1996.
DOI : 10.1007/978-1-4684-0357-2

G. Dowek, T. Hardin, and C. Kirchner, HOL-?? an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, issue.1, pp.1-25, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00098847

G. Dowek and B. Werner, Arithmetic as a Theory Modulo, RTA, pp.423-437, 2005.
DOI : 10.1007/978-3-540-32033-3_31

G. Burel, A First-Order Representation of Pure Type Systems Using Superdeduction, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.253-263, 2008.
DOI : 10.1109/LICS.2008.22
URL : https://hal.archives-ouvertes.fr/inria-00198543