J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

P. B. Andrews, General models, descriptions, and choice in type theory, The Journal of Symbolic Logic, vol.52, issue.02, pp.385-394, 1972.
DOI : 10.1305/ndjfl/1093957876

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

H. P. Barendregt, Introduction to generalized type systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991.

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

Z. Chihani, D. Miller, and F. Renaud, Checking foundational proof certificates for first-order logic (extended abstract), Third International Workshop on Proof Exchange for Theorem Proving, pp.58-66, 2013.

Z. Chihani, D. Miller, and F. Renaud, Foundational Proof Certificates in First-Order Logic, Conference on Automated Deduction 2013, number 7898 in LNAI, pp.162-177, 2013.
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, 8th International Conference Proceedings, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

N. G. De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem, Indagationes Mathematicae, vol.34, issue.5, pp.381-392, 1972.

E. Deplagne, C. Kirchner, H. Kirchner, and Q. H. Nguyen, Proof Search and Proof Check for Equational and Inductive Theorems, CADE-19, pp.297-316, 2003.
DOI : 10.1007/978-3-540-45085-6_26
URL : https://hal.archives-ouvertes.fr/inria-00099470

]. Girard, A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs, 1992.

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

C. Kirchner and H. Kirchner, Equational Logic and Rewriting, Logic and Computation, volume 9 of Handbook of the History of Logic, pp.255-282, 2014.
DOI : 10.1016/B978-0-444-51624-4.50006-X
URL : https://hal.archives-ouvertes.fr/hal-01183817

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041

D. Miller, A Proposal for Broad Spectrum Proof Certificates, CPP: First International Conference on Certified Programs and Proofs, pp.54-69, 2011.
DOI : 10.1007/978-3-540-88387-6_3
URL : https://hal.archives-ouvertes.fr/hal-00772722

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W

G. Robinson and L. Wos, Paramodulation and theorem-proving in first-order theories with equality, Automation of Reasoning, pp.298-313, 1983.

P. Schroeder-heister, Rules of definitional reflection, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.222-232, 1993.
DOI : 10.1109/LICS.1993.287585

T. Sternagel, S. Winkler, and H. Zankl, Recording Completion for Certificates in Equational Reasoning, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pp.41-47, 2015.
DOI : 10.1145/2676724.2693171

R. Thiemann and C. Sternagel, Certification of Termination Proofs Using CeTA, Theorem Proving in Higher Order Logics, TPHOLs, pp.452-468, 2009.
DOI : 10.1007/978-3-540-25979-4_6

Y. Toyama, Counterexamples to termination for the direct sum of term rewriting systems, Information Processing Letters, vol.25, issue.3, pp.141-143, 1987.
DOI : 10.1016/0020-0190(87)90122-0