F. Stuart, R. L. Allen, D. J. Constable, W. E. Howe, and . Aitken, The Semantics of Reected Proof, LICS, p.95105, 1990.

. E. Acp-+-08-]-b, A. Aydemir, B. C. Charguéraud, R. Pierce, S. Pollack et al., Engineering formal metatheory, POPL, p.315, 2008.

J. [. Ayache and . Filliâtre, Combining the Coq proof assistant with rst-order decision procedures. Unpublished notes, 2006.

G. Armand, B. Faure, C. Grégoire, L. Keller, B. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Jouannaud and Shao [JS11], p.135150
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

G. Armand, B. Faure, C. Grégoire, L. Keller, B. Théry et al., Verifying SAT and SMT in Coq for a fully automated decision procedure, PSATTT -International Workshop on Proof-Search in Axiomatic Theories and Type Theories -2011, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00614041

[. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verication, p.8398
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.inria.fr/inria-00502496/file/fastcoq.pdf

A. Fadi, K. A. Aloul, I. L. Sakallah, and . Markov, Ecient Symmetry Breaking for Boolean Satisability, IEEE Trans. Computers, vol.55, issue.5, p.549558, 2006.

G. Henry and . Baker, Shallow binding makes functional arrays fast, SIGPLAN Notices, vol.26, issue.8, p.145147, 1991.

B. Barras, Auto-validation d'un système de preuves avec familles inductives, 1999.

B. Brummayer and A. Biere, Fuzzing and delta-debugging SMT solvers, Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT '09, p.15, 2009.
DOI : 10.1145/1670412.1670413
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.365.625

[. Blanchette, S. Böhme, and L. C. Paulson, Extending Sledgehammer with SMT Solvers, Bjørner and Sofronie-Stokkermans [BSS11], p.116130
DOI : 10.1007/BFb0028402
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.194.1769

A. Bcc-+-99-]-armin-biere, E. M. Cimatti, M. Clarke, Y. Fujita, and . Zhu, Symbolic model checking using sat procedures instead of bdds, DAC, p.317320, 1999.

M. Boespug, Q. Carbonneaux, and O. Hermant, The ??-calculus modulo as a universal proof language, Proof Exchange for Theorem ProvingSecond International Workshop, p.2843, 2012.

[. Besson, P. Cornilleau, and D. Pichardie, Modular SMT Proofs for Fast Reexive Checking Inside Coq, Jouannaud and Shao [JS11], p.151166

[. Boespug, M. Dénès, and B. Grégoire, Full Reduction at Full Throttle, Jouannaud and Shao [JS11], p.362377

]. T. Bdodf09, D. C. Bouton, D. De-oliveira, P. Déharbe, and . Fontaine, veriT: An Open, Trustable and Ecient SMT-Solver, Lecture Notes in Computer Science, vol.5663, p.151156, 2009.

N. Benton, Machine Obstructed Proof, Workshop on Mechanizing Metatheory, 2006.

]. F. Bes06 and . Besson, Fast Reexive Arithmetic Tactics the Linear Case and Beyond, Lecture Notes in Computer Science, vol.4502, p.4862, 2006.

J. Richard, A. D. Boulton, M. J. Gordon, J. Gordon, J. Harrison et al., Experience with embedding hardware description languages in hol, TPCD, volume A-10 of IFIP Transactions, pp.129-156, 1992.

J. Bernardy, P. Jansson, and R. Paterson, Parametricity and dependent types, p.345356, 2010.

A. Braunstein, M. Mézard, and R. Zecchina, Survey propagation: An algorithm for satisability. Random Struct, Algorithms, vol.27, issue.2, p.201226, 2005.
DOI : 10.1002/rsa.20057
URL : http://arxiv.org/abs/cs/0212002

R. E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8
DOI : 10.1109/TC.1986.1676819

H. [. Berger and . Schwichtenberg, An inverse of the evaluation functional for typed lambda -calculus, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, p.203211, 1991.
DOI : 10.1109/LICS.1991.151645

C. Barrett, A. Stump, and C. Tinelli, The SMT-LIB Standard: Version 2.0, Proceedings of the 8th International Workshop on Satisability Modulo Theories, 2010.

T. [. Böhme and . Weber, Fast LCF-Style Proof Reconstruction for Z3, p.179194
DOI : 10.1007/978-3-642-14052-5_14

D. Chai and A. Kuehlmann, A fast pseudo-Boolean constraint solver

[. Cotton, Two Techniques for Minimizing Resolution Proofs, Lecture Notes in Computer Science, vol.6175, p.306312, 2010.
DOI : 10.1007/978-3-642-14186-7_26

M. [. Clarke, H. Talupur, D. Veith, and . Wang, Sat based predicate abstraction for hardware verication, Theory and Applications of Satisability Testing, p.267268, 2004.

Z. Dargaye, Vérication formelle d'un compilateur pour langages fonctionnels, 2009.

]. N. De-bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions, Symposium on automatic demonstration, p.2961, 1970.

]. M. Dén and . Dénès, Coq with imperative data structures

]. E. Den00 and . Denney, A prototype proof translator from hol to coq, Aagaard and Harrison [AH00], p.108125

A. Darbari, B. Fischer, and J. Marques-silva, Industrial-Strength Certied SAT Solving through Veried SAT Proof Checking, Lecture Notes in Computer Science, vol.6255, p.260274, 2010.

R. Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society, p.176178, 1975.
DOI : 10.1090/S0002-9939-1975-0373893-X

G. [. Davis, D. Logemann, and . Loveland, A machine program for theoremproving, dMB08] Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: An ecient smt solver, p.394397, 1962.

H. [. Davis and . Putnam, A computing procedure for quantication theory, Journal of the ACM (JACM), vol.7, issue.3, p.201215, 1960.

[. Dershowitz and I. Tzameret, Complexity of propositional proofs under a promise, ACM Transactions on Computational Logic, vol.11, issue.3, 2010.
DOI : 10.1145/1740582.1740586

[. Filliâtre and S. Conchon, Type-safe modular hash-consing, Proceedings of the 2006 workshop on ML , ML '06, p.1219, 2006.
DOI : 10.1145/1159876.1159880

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verication, Damm and Hermanns [DH07], p.173177

]. P. Fmm-+-06, J. Fontaine, S. Marion, L. P. Merz, A. F. Nieto et al., Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS, p.167181, 2006.

[. Fontaine, S. Merz, and B. W. Paleo, Compression of Propositional Resolution Proofs via Partial Regularization, Bjørner and Sofronie-Stokkermans [BSS11], p.237251
DOI : 10.1007/978-3-642-14186-7_26
URL : https://hal.archives-ouvertes.fr/inria-00617846

U. Furbach and N. Shankar, Automated Reasoning, Third International Joint Conference Proceedings, 2006.
DOI : 10.1007/11814771

A. J. Gill, J. Launchbury, and S. L. Jones, A short cut to deforestation, Proceedings of the conference on Functional programming languages and computer architecture , FPCA '93, p.223232, 1993.
DOI : 10.1145/165180.165214

S. Glondu, Extraction certiée dans coq-en-coq JFLA, volume 7.2 of Studia Informatica Universalis Gonthier and A. Mahboubi. A small scale reection extension for the Coq system, p.383410, 2008.

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A modular formalisation of nite group theory, p.86101

G. Gonthier, Formal Proof The Four-Color Theorem, Notices of the AMS, vol.55, issue.11, p.13821393, 2008.

A. Rinard and . Solar-lezama, Lynx: A Programmatic SAT Solver for the RNA-Folding Problem, Lecture Notes in Computer Science, vol.7317, p.143156, 2012.

B. Grégoire, Compilation des termes de preuves: un (nouveau) mariage entre Coq et Ocaml, Thése de doctorat, spécialité informatique, 2003.

B. [. Garillot and . Werner, Simple Types in Type Theory: Deep and Shallow Encodings, Schneider and Brandt [SB07], p.368382
DOI : 10.1007/978-3-540-74591-4_27

]. J. Har06 and . Harrison, Towards self-verication of HOL Light, p.177191

C. Thomas, J. Hales, S. Harrison, T. Mclaughlin, S. Nipkow et al., A Revision of the Proof of the Kepler Conjecture, Discrete & Computational Geometry, vol.44, issue.1, p.134, 2010.

L. [. Harrison and . Théry, A Sceptic's Approach to Combining HOL and Maple, Journal of Automated Reasoning, vol.21, issue.3, p.279294, 1998.

J. Hurd, OpenTheory: Package management for higher order logic theories

C. Keller and M. Lasson, Parametricity in an Impredicative Sort, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, p.381395, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00730913

V. Kuncak, M. Mayer, R. Piskac, and P. Suter, Comfusy: A Tool for Complete Functional Synthesis, Lecture Notes in Computer Science, vol.6174, p.430433, 2010.
DOI : 10.1007/978-3-642-14295-6_38

D. Kroening and O. Strichman, Decision Procedures: an Algorithmic Point of View, 2008.
DOI : 10.1007/978-3-662-50497-0

C. Keller and B. Werner, Importing HOL Light into Coq, p.307322
DOI : 10.1007/978-3-642-14052-5_22
URL : https://hal.archives-ouvertes.fr/inria-00520604

S. Lescuyer and S. Conchon, Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, Lecture Notes in Computer Science, vol.7, issue.3, pp.287-303, 2009.
DOI : 10.1016/j.jal.2007.07.003

[. Leroy, Formal verication of a realistic compiler

P. Letouzey, Programmation fonctionnelle certiée L'extraction de programmes dans l'assistant Coq, 2004.

J. Lambek and P. J. Scott, Introduction to higher order categorical logic

C. [. Mclaughlin, Y. Barrett, and . Ge, Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite, Electronic Notes in Theoretical Computer Science, vol.144, issue.2, p.4351, 2006.
DOI : 10.1016/j.entcs.2005.12.005

]. R. Mil72 and . Milner, Logic for Computable Functions: Description of a Machine Implementation, 1972.

[. Miller, A Proposal for Broad Spectrum Proof Certicates, Jouannaud and Shao [JS11], p.5469

S. Müller and I. Tzameret, Short Propositional Refutations for Dense Random 3CNF Formulas, LICS, p.501510, 2012.

G. Nelson and D. C. Oppen, Simplication by Cooperating Decision Procedures, ACM Trans. Program. Lang. Syst, vol.1, issue.2, p.245257, 1979.
DOI : 10.1145/357073.357079
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.2828

A. [. Nieuwenhuis, C. Oliveras, and . Tinelli, Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, p.937977, 2006.
DOI : 10.1145/1217856.1217859

S. [. Obua and . Skalberg, Importing HOL into Isabelle/HOL, Furbach and Shankar [FS06], p.298302
DOI : 10.1007/11814771_27

C. John and . Reynolds, Types, abstraction and parametric polymorphism, IFIP Congress, p.513523, 1983.

[. Robinson and C. Gretton, Duc Nghia Pham, and Abdul Sattar. A compact and ecient sat encoding for planning, p.296303

M. [. Rondon, R. Kawaguchi, and . Jhala, Liquid types
DOI : 10.1145/1379022.1375602

]. A. Spi06 and . Spiwack, Ajouter des entiers machine à Coq, 2006.

G. Tseitin, On the Complexity of Proofs in Propositional Logics, Seminars in Mathematics, p.466483, 1970.

P. Wadler, Theorems for free! In FPCA, p.347359, 1989.

T. Weber, A SAT-based Sudoku solver, LPAR, p.1115, 2005.

T. Weber, SAT-based Finite Model Generation for Higher-Order Logic, 2008.

F. Wiedijk, Encoding the hol light logic in coq. Unpublished notes, 2007.