J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, J. of Logic and Computation, vol.2, pp.297-347, 1992.

B. Peter and . Andrews, Theorem Proving via General Matings, J. ACM, vol.28, pp.193-214, 1981.

J. Avigad, Eliminating Definitions and Skolem Functions in First-Order Logic, ACM Transactions on Computational Logic, vol.4, pp.402-415, 2003.

M. Baaz, S. Hetzl, and D. Weller, On the complexity of proof deskolemization, J. of Symbolic Logic, vol.77, pp.669-686, 2012.

M. Baaz and A. Leitsch, On Skolemization and Proof Complexity, Fundamenta Informaticae, vol.20, pp.353-379, 1994.

H. Barbosa, J. C. Blanchette, and P. Fontaine, Scalable Fine-Grained Proofs for Formula Processing, 26th International Conference on Automated Deduction (CADE) (LNCS), vol.10395, pp.398-412, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01526841

R. Blanco, Z. Chihani, and D. Miller, Translating Between Implicit and Explicit Versions of Proof, Automated Deduction -CADE 26 -26th International Conference on Automated Deduction, vol.10395, pp.255-273, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01645016

K. Chaudhuri, S. Hetzl, and D. Miller, A Multi-Focused Proof System Isomorphic to Expansion Proofs, J. of Logic and Computation, vol.26, pp.577-603, 2016.
URL : https://hal.archives-ouvertes.fr/hal-00937056

Z. Chihani, T. Libal, and G. Reis, The proof certifier Checkers, Proceedings of the 24th Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) (LNCS), pp.201-210, 2015.
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, pp.93-108, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01390919

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, vol.14, pp.58-66, 2013.

Z. Chihani, D. Miller, and F. Renaud, A semantic framework for proof evidence, J. of Automated Reasoning, vol.59, pp.287-330, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01390912

A. Church, A Formulation of the Simple Theory of Types, J. of Symbolic Logic, vol.5, pp.56-68, 1940.

N. Hans-de, Extraction of Proofs from the Clausal Normal Form Transformation, CSL: 16th Workshop on Computer Science Logic, vol.2471, pp.584-598, 2002.

N. Hans-de, Translation of resolution proofs into short firstorder proofs without choice axioms, Information and Computation, vol.199, pp.24-54, 2005.

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: Fast, Embeddable, ?Prolog Interpreter, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference, vol.9450, pp.460-468, 2015.

G. Ebner, S. Hetzl, G. Reis, M. Riener, S. Wolfsteiner et al., System Description: GAPT 2.0, Proceedings of the 8th International Joint Conference on Automated Reasoning, IJCAR 2016 (LNCS), vol.9706, pp.293-301, 2016.

M. Färber and C. Kaliszyk, No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions, Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR) (CEUR Workshop Proceedings, vol.1635, pp.24-31, 2016.

P. Fontaine, J. Marion, S. Merz, L. P. Nieto, and A. Tiu, Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS: Tools and Algorithms for the Construction and Analysis of Systems, vol.3920, pp.167-181, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00001088

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

J. Girard, A new constructive logic: classical logic, Math. Structures in Comp. Science, vol.1, pp.255-296, 1991.
URL : https://hal.archives-ouvertes.fr/inria-00075117

J. Goubault, A BDD-Based Simplification and Skolemization Procedure, Logic Journal of the IGPL, vol.3, pp.827-855, 1995.

U. Kohlenbach and P. Oliva, Proof mining in L 1 -approximation, Annals of Pure and Applied Logic, vol.121, pp.1-38, 2003.

C. Liang and D. Miller, Focusing and Polarization in Linear, Intuitionistic, and Classical Logics, Theoretical Computer Science, vol.410, pp.4747-4768, 2009.

D. Miller, Proofs in Higher-order Logic, Ph.D. Dissertation. Carnegie-Mellon University, 1983.

D. Miller, A Compact Representation of Proofs, Studia Logica, vol.46, pp.347-370, 1987.

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

D. Miller, Unification of Simply Typed Lambda-Terms as Logic Programming, Eighth International Logic Programming Conference, pp.255-269, 1991.

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

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), pp.287-291, 1999.

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, Handbook of Automated Reasoning, 2001.

, I. Elsevier Science B.V., Chapter, vol.6, pp.335-367

G. Reger and M. Suda, Checkable Proofs for First-Order Theorem Proving, ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (EPiC Series in Computing), vol.51, pp.55-63, 2017.

J. R. Shoenfield, Mathematical Logic, 1967.

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

E. Tassi, Elpi: an extension language for Coq, The Fourth International Workshop on Coq for Programming Languages, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01637063