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

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Certified Programs and Proofs (CPP 2011), pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

D. Baelde, Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, issue.1, 2012.

H. Barendregt, Abstract, Bulletin of Symbolic Logic, vol.27, issue.02, pp.181-215, 1997.
DOI : 10.1093/comjnl/32.2.98

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.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

R. Blanco and D. Miller, Proof Outlines as Proof Certificates: A System Description, Proceedings First International Workshop on Focusing of Electronic Proceedings in Theoretical Computer Science, pp.7-14, 2015.
DOI : 10.4204/EPTCS.197.2
URL : https://hal.archives-ouvertes.fr/hal-01238436

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

S. Böhme and T. Weber, Designing proof formats: A user's perspective, PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, pp.27-32, 2011.

K. Chaudhuri, Classical and Intuitionistic Subexponential Logics Are Equally Expressive, CSL 2010: Computer Science Logic, pp.185-199, 2010.
DOI : 10.1007/978-3-642-15205-4_17
URL : https://hal.archives-ouvertes.fr/inria-00534865

K. Chaudhuri, S. Hetzl, and D. Miller, A multi-focused proof system isomorphic to expansion proofs, Journal of Logic and Computation, vol.26, issue.2, pp.577-603, 2016.
DOI : 10.1093/logcom/exu030
URL : https://hal.archives-ouvertes.fr/hal-00937056

K. Chaudhuri, D. Miller, and A. Saurin, Canonical Sequent Proofs via Multi-Focusing, Fifth International Conference on Theoretical Computer Science, IFIP 273, pp.383-396, 2008.
DOI : 10.1007/978-0-387-09680-3_26
URL : https://hal.archives-ouvertes.fr/hal-00527893

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, Certification of First-order proofs in classical and intuitionistic logics, 2015.

Z. Chihani, T. Libal, and G. Reis, The Proof Certifier Checkers, Proceedings of the 24th Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), pp.201-210, 2015.
DOI : 10.1007/978-3-319-24312-2_14
URL : https://hal.archives-ouvertes.fr/hal-01208333

Z. Chihani and D. Miller, Proof Certificates for Equality Reasoning, Post-proceedings of LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications. Natal, 2016.
DOI : 10.1016/j.entcs.2016.06.007
URL : https://hal.archives-ouvertes.fr/hal-01390919

Z. Chihani, D. Miller, and F. Renaud, Checking foundational proof certificates for firstorder 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, LNAI 7898, pp.162-177, 2013.
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485

Z. Chihani, D. Miller, and F. Renaud, Supporting ?Prolog code, 2016.

N. Chomsky, Three models for the description of language, IEEE Transactions on Information Theory, vol.2, issue.3, pp.113-124, 1956.
DOI : 10.1109/TIT.1956.1056813

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

S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems, The Journal of Symbolic Logic, vol.87, issue.01, pp.36-50, 1979.
DOI : 10.1007/BF01475439

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

V. Danos, J. Joinet, and H. Schellinx, LKT and LKQ: sequent calculi for second order logic based upon dual linear decompositions of classical implication, Advances in Linear Logic, number 222 in London Mathematical Society Lecture Note Series, pp.211-224, 1995.

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.

O. Delande, D. Miller, and A. Saurin, Proof and refutation in MALL as a game, Annals of Pure and Applied Logic, vol.161, issue.5, pp.654-672, 2010.
DOI : 10.1016/j.apal.2009.07.017
URL : https://hal.archives-ouvertes.fr/hal-00527922

G. Dowek, Skolemization in simple type theory: the logical and the theoretical points of view, Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, number 17 in Studies in Logic, pp.244-255, 2008.

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/hal-01199524

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, J. of Automated Reasoning, vol.31, issue.1, pp.31-72, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01199506

C. Dunchev, F. Guidi, C. S. Coen, and E. Tassi, ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter, Logic for Programming , Artificial Intelligence, and Reasoning -20th International Conference Proceedings, pp.460-468, 2015.
DOI : 10.1007/978-3-662-48899-7_32

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. Felty, Transforming specifications in a dependent-type lambda calculus to specifications in an intuitionistic logic, Logical Frameworks, 1991.

A. Felty, Encoding the calculus of constructions in a higher-order logic, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.233-244, 1993.
DOI : 10.1109/LICS.1993.287584

A. Felty, Implementing tactics and tacticals in a higher-order logic programming language, Journal of Automated Reasoning, vol.5, issue.3, pp.43-81, 1993.
DOI : 10.1007/BF00881900

P. Fontaine, J. Marion, S. Merz, L. P. Nieto, and A. F. Tiu, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, pp.167-181, 2006.
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088

J. H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, 1986.

A. V. Gelder, Producing and verifying extremely large propositional refutations, Annals of Mathematics and Artificial Intelligence, vol.43, issue.1???4, pp.329-372, 2012.
DOI : 10.1007/s10472-012-9322-x

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

G. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol.25, issue.1, pp.493-565, 1936.
DOI : 10.1007/BF01565428

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

J. Girard, P. Taylor, and Y. Lafont, Proofs and Types, 1989.

M. Gordon, From LCF to HOL: a short history, Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp.169-186, 2000.

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

Q. Heath and D. Miller, A framework for proof certificates in finite state exploration, Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, number 186 in Electronic Proceedings in Theoretical Computer Science, pp.11-26, 2015.
DOI : 10.4204/EPTCS.186.4
URL : https://hal.archives-ouvertes.fr/hal-01240172

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.

W. Hodges, Logic and games, 2013.

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

D. J. Hughes, Proofs without syntax, Annals of Mathematics, vol.164, issue.3, pp.1065-1076, 2006.
DOI : 10.4007/annals.2006.164.1065

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

S. C. Johnson, Yacc: Yet another compiler-compiler, NJ, vol.32, 1975.

G. Kahn, Natural semantics, Proceedings of the Symposium on Theoretical Aspects of Computer Science, pp.22-39, 1987.
DOI : 10.1007/BFb0039592
URL : https://hal.archives-ouvertes.fr/inria-00075953

A. N. Kolmogorov, On the principle of the excluded middle Matematicheskii sbornik, English translation by Jean van Heijenoort in From Frege to Gödel, pp.646-667, 1925.

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

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

C. Liang and D. Miller, A focused approach to combining logics, Annals of Pure and Applied Logic, vol.162, issue.9, pp.679-697, 2011.
DOI : 10.1016/j.apal.2011.01.012
URL : https://hal.archives-ouvertes.fr/hal-00772736

P. Lorenzen, Ein dialogisches konstruktivitätskriterium, Infinitistic Methods: Proceed. Symp. Foundations of Math, pp.193-200, 1961.

D. Miller, A compact representation of proofs, Studia Logica, vol.19, issue.4, pp.347-370, 1987.
DOI : 10.1007/BF00370646

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, Proof checking and logic programming, Logic-Based Program Synthesis and Transformation (LOPSTR), pp.3-17, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01390901

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

D. Miller and A. Saurin, From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic, CSL 2007: Computer Science Logic, pp.405-419, 2007.
DOI : 10.1007/978-3-540-74915-8_31
URL : https://hal.archives-ouvertes.fr/hal-00527888

D. Miller and M. Volpe, Focused Labeled Proof Systems for Modal Logic, Logic for Programming, Artificial Intelligence , and Reasoning (LPAR), 2015.
DOI : 10.1007/978-3-662-48899-7_19
URL : https://hal.archives-ouvertes.fr/hal-01213858

R. Milner, M. Tofte, R. Harper, and D. Macqueen, The Definition of Standard ML (Revised), 1997.

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

G. C. Necula and S. P. , Oracle-based checking of untrusted software, 28th ACM Symp. on Principles of Programming Languages, pp.142-154, 2001.

L. C. Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, vol.49, issue.3, pp.363-397, 1989.
DOI : 10.1007/BF00248324

F. C. Pereira and S. M. Shieber, Prolog and Natural-Language Analysis, CLSI, vol.10, 1987.

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

G. D. Plotkin, A structural approach to operational semantics. DAIMI FN-19, 1981.

G. D. Plotkin, The origins of structural operational semantics, J. of Logic and Algebraic Programming, vol.60, pp.3-15, 2004.

D. Prawitz, Natural Deduction, Almqvist & Wiksell, 1965.

X. Qi, A. Gacek, S. Holte, G. Nadathur, and Z. Snow, The Teyjus system ? version 2, 2015.

F. Rabe, The Future of Logic: Foundation-Independence, Logica Universalis, vol.230, issue.1, pp.1-20, 2016.
DOI : 10.1007/s11787-015-0132-x

R. Saillard, Towards explicit rewrite rules in the ??-calculus modulo, IWIL-10th International Workshop on the Implementation of Logics, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00921340

S. M. Shieber, Y. Schabes, and F. C. Pereira, Principles and implementation of deductive parsing, The Journal of Logic Programming, vol.24, issue.1-2, pp.3-36, 1995.
DOI : 10.1016/0743-1066(95)00035-I

J. Slaney, Solution to a problem of Ono and Komori, Journal of Philosophical Logic, vol.14, issue.1, pp.103-111, 1989.
DOI : 10.1007/BF00296176

Z. Snow, D. Baelde, and G. Nadathur, A meta-programming approach to realizing dependently typed logic programming, Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '10, pp.187-198, 2010.
DOI : 10.1145/1836089.1836113

J. E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, 1977.

A. Stump, Proof Checking Technology for Satisfiability Modulo Theories, Logical Frameworks and Meta-Languages: Theory and Practice, 2008.
DOI : 10.1016/j.entcs.2008.12.121

A. Stump, D. Oe, A. Reynolds, L. Hadarean, and C. Tinelli, SMT proof checking using a logical framework. Formal Methods in System Design, pp.91-118, 2013.

A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2000.
DOI : 10.1017/CBO9781139168717

N. Wetzler, M. J. Heule, and J. W. 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