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

A. Assaf, A framework for defining computational higher-order logics, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01235303

D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur et al., Abella: A system for reasoning about relational specifications, Journal of Formalized Reasoning, vol.7, issue.2, p.2014
URL : https://hal.archives-ouvertes.fr/hal-01102709

R. Blanco and D. Miller, Proof outlines as proof certificates: a system description. Draft available online, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01238436

R. S. Boyer and J. S. Moore, A Computational Logic, 1979.

K. Chaudhuri, F. Pfenning, and G. Price, A Logical Characterization of Forward and Backward Chaining in the Inverse Method, Journal of Automated Reasoning, vol.2, issue.5, pp.133-177, 2008.
DOI : 10.1007/s10817-007-9091-0

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

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

D. Cousineau and G. Dowek, Embedding pure type systems in the lambda-picalculus modulo, Typed Lambda Calculi and Applications , 8th International Conference Proceedings, pp.102-117, 2007.

V. Danos, J. Joinet, and H. Schellinx, LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, A fast interpreter for ?Prolog, LPAR-20: Logic Programming and Automated Reasoning, International Conference, 2015.

R. Dyckhoff and S. Lengrand, Call-by-Value ??-calculus and LJQ, Journal of Logic and Computation, vol.17, issue.6, pp.1109-1134, 2007.
DOI : 10.1093/logcom/exm037
URL : https://hal.archives-ouvertes.fr/hal-00150284

A. Gacek, D. Miller, and G. Nadathur, A Two-Level Logic Approach to Reasoning About Computations, Journal of Automated Reasoning, vol.40, issue.4, pp.241-273, 2012.
DOI : 10.1007/s10817-011-9218-1
URL : https://hal.archives-ouvertes.fr/hal-00776208

G. Gentzen, Investigations into logical deduction The Collected Papers of Gerhard Gentzen, pp.68-131, 1935.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, 8th Asian Symposium on Computer Mathematics, p.333, 2007.
DOI : 10.1007/978-3-540-87827-8_28

T. C. Hales, A proof of the Kepler conjecture, Annals of Mathematics, vol.162, issue.3, pp.1065-1185, 2005.
DOI : 10.4007/annals.2005.162.1065

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

H. Herbelin, Séquents qu'on calcule: de l'interprétation du calcul des séquents comme calcul de lambda-termes et comme calcul de stratégies gagnantes, 1995.

J. M. Howe, Proof Search Issues in Some Non-Classical Logics, 1998.

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.207-220, 2009.
DOI : 10.1145/1629575.1629596

O. Laurent, Etude de la polarisation en logique, 2002.
URL : https://hal.archives-ouvertes.fr/tel-00007884

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

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

J. Meng, The integration of higher order interactive proof with first order automatic theorem proving, 2015.

D. Miller, Abstractions in logic programming, Logic and Computer Science, pp.329-359, 1990.

D. Miller, Communicating and trusting proofs: The case for broad spectrum proof certificates, Logic, Methodology, and Philosophy of Science. Proceedings of the Fourteenth International Congress, pp.323-342, 2014.

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. Nadathur and D. J. Mitchell, System Description: Teyjus???A Compiler and Abstract Machine Based Implementation of ??Prolog, 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, pp.287-291, 1999.
DOI : 10.1007/3-540-48660-7_25

F. Pereira, C-Prolog User's Manual, Version 1, 1988.

F. Pfenning and C. Schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

N. Wetzler, M. J. Heule, J. A. Warren, and . Hunt, DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs, Theory and Applications of Satisfiability Testing SAT 2014, pp.422-429, 2014.
DOI : 10.1007/978-3-319-09284-3_31