C. Ballarin, Locales: A Module System for Mathematical Theories, Journal of Automated Reasoning, vol.254, issue.2, pp.123-153, 2014.
DOI : 10.1007/s10817-013-9284-7

B. Jr, R. J. Schrag, and R. , Using CSP look-back techniques to solve exceptionally hard SAT instances, ) CP96. LNCS, pp.46-60, 1996.

J. C. Blanchette, S. Böhme, M. Fleury, S. J. Smolka, and A. Steckermeier, Semi-intelligible Isar Proofs from Machine-Generated Proofs, Journal of Automated Reasoning, vol.27, issue.4
DOI : 10.1007/s10817-015-9335-3
URL : https://hal.archives-ouvertes.fr/hal-01211748

J. C. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, J. Autom. Reasoning, vol.37, issue.1-2, pp.109-128, 2013.
DOI : 10.1007/BFb0028402

J. C. Blanchette, L. Bulwahn, and T. Nipkow, Automatic Proof and Disproof in Isabelle/HOL, FroCoS 2011, pp.12-27, 2011.
DOI : 10.1007/BFb0028402

J. C. Blanchette and A. Popescu, Mechanizing the Metatheory of Sledgehammer, FroCoS 2013, pp.245-260, 2013.
DOI : 10.1007/978-3-642-40885-4_17

J. C. Blanchette, M. Fleury, A. Schlichtkrull, and D. Traytel, IsaFoL: Isabelle Formalization of Logic

J. C. Blanchette, A. Popescu, and D. Traytel, Unified Classical Logic Completeness, IJCAR 2014, pp.46-60, 2014.
DOI : 10.1007/978-3-319-08587-6_4

S. Böhme and T. Weber, Fast LCF-Style Proof Reconstruction for Z3, ITP 2010, pp.179-194, 2010.
DOI : 10.1007/978-3-642-14052-5_14

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

M. Davis, G. Logemann, and D. W. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

M. Fleury, Formalisation of ground inference systems in a proof assistant

M. Fleury and J. C. Blanchette, Formalization of Weidenbach's Automated Reasoning?The Art of Generic Problem Solving

F. Haftmann and T. Nipkow, Code Generation via Higher-Order Rewrite Systems, FLOPS 2010, pp.103-117, 2010.
DOI : 10.1007/978-3-642-12251-4_9

J. Harrison, Formalizing basic first order model theory, TPHOLs '98, pp.153-170, 1998.
DOI : 10.1007/BFb0055135

M. Heule, H. Jr, W. A. Wetzler, and N. , Bridging the gap between easy generation and efficient verification of unsatisfiability proofs, Software Testing, Verification and Reliability, vol.411, issue.50, pp.593-607, 2014.
DOI : 10.1002/stvr.1549

F. Kammüller, M. Wenzel, and L. C. Paulson, Locales A Sectioning Concept for Isabelle, TPHOLs '99, pp.149-166, 1999.
DOI : 10.1007/3-540-48256-3_11

D. E. Knuth, The Art of Computer Programming, 2015.

A. Krauss, Partial Recursive Functions in Higher-Order Logic, IJCAR 2006, pp.589-603, 2006.
DOI : 10.1007/11814771_48

S. Lescuyer, Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq, 2011.
URL : https://hal.archives-ouvertes.fr/tel-00713668

M. Luby, A. Sinclair, and D. Zuckerman, Optimal speedup of Las Vegas algorithms, Information Processing Letters, vol.47, issue.4, pp.173-180, 1993.
DOI : 10.1016/0020-0190(93)90029-9

J. Margetson and T. Ridge, Completeness theorem, 2004.

F. Mari´cmari´c, Formal verification of modern SAT solvers Archive of Formal Proofs, pp.develop- ment, 2008.

F. Mari´cmari´c, Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL, Theoretical Computer Science, vol.411, issue.50, pp.4333-4356, 2010.
DOI : 10.1016/j.tcs.2010.09.014

J. P. Marques-silva and K. A. Sakallah, GRASP?A new search algorithm for satisfiability, ICCAD '96, pp.220-227, 1996.

R. Matuszewski and P. Rudnicki, Mizar: The first 30 years, Mechanized Mathematics and Its Applications, vol.4, issue.1, pp.3-24, 2005.

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff, Proceedings of the 38th conference on Design automation , DAC '01, pp.530-535, 2001.
DOI : 10.1145/378239.379017

R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006.
DOI : 10.1145/1217856.1217859

T. Nipkow, Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs, VMCAI 2012, pp.24-38, 2012.
DOI : 10.3233/JCS-1996-42-304

T. Nipkow and G. Klein, Concrete Semantics, 2014.
DOI : 10.1007/978-3-319-10542-0

D. Oe, A. Stump, C. Oliver, and K. Clancy, versat: A Verified Modern SAT Solver, VMCAI 2012, pp.363-378, 2012.
DOI : 10.1016/j.scico.2007.07.008

L. C. Paulson and J. C. Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, IWIL-2010. EPiC, pp.1-11, 2012.

B. C. Pierce, Lambda, the ultimate TA: Using a proof assistant to teach programming language foundations, pp.121-122, 2009.

A. Reynolds, C. Tinelli, and L. De-moura, Finding conflicting instances of quantified formulas in SMT, 2014 Formal Methods in Computer-Aided Design (FMCAD), pp.195-202, 2014.
DOI : 10.1109/FMCAD.2014.6987613

N. Shankar, Metamathematics, Machines, and Gödel's Proof, Cambridge Tracts in Theoretical Computer Science, vol.38, 1994.

N. Shankar and M. Vaucher, The Mechanical Verification of a DPLL-Based Satisfiability Solver, Electronic Notes in Theoretical Computer Science, vol.269, pp.3-17, 2011.
DOI : 10.1016/j.entcs.2011.03.002

C. Sternagel and R. Thiemann, An Isabelle/HOL formalization of rewriting for certified termination analysis

A. Voronkov, AVATAR: The Architecture for First-Order Theorem Provers, CAV 2014, pp.696-710, 2014.
DOI : 10.1007/978-3-319-08867-9_46

C. Weidenbach, Automated Reasoning Building Blocks, Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, pp.172-188, 2015.
DOI : 10.1007/978-3-319-23506-6_12
URL : https://hal.archives-ouvertes.fr/hal-01239428

M. Wenzel, Isabelle/Isar?A generic framework for human-readable proof documents From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric, 2007.

J. Woodcock and R. Banach, The verification grand challenge, J. Univers. Comput. Sci, vol.13, issue.5, pp.661-668, 2007.