M. Aagaard, M. Leeser, and P. Windley, Toward a super duper hardware tactic, Proc. 6th Int. Workshop on Higher Order Logic Theorem Proving and its Applications, pp.400-414, 1993.
DOI : 10.1007/3-540-57826-9_151
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.3427

S. Mads and . Ager, From natural semantics to abstract machines, Proc. 3rd Int. Symp. on Logic-based Program Synthesis and Transformation, pp.245-261, 2004.

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. Archer, B. D. Vito, and C. Muñoz, Developing user strategies in PVS: A tutorial, Proc. Int. Workshop on Design and Application of Strategies/Tactics in Higher Order Logics, number CP-2003-212448 in NASA Conference Publication, pp.16-42, 2003.

Z. Ariola and A. Sabry, Correctness of monadic state, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.62-74, 1998.
DOI : 10.1145/268946.268952

N. Ayache and J. Filliâtre, Combining the coq proof assistant with first-order decision procedures, 0140.

J. Belinfante, Computer proofs in Gödel's class theory with equational definitions for composite and cross, Journal of Automated Reasoning, vol.22, issue.3, pp.311-339, 1999.
DOI : 10.1023/A:1006050629424

P. Bernays, Axiomatic Set Theory, p.126, 1958.

S. Boldo and C. Muñoz, Provably faithful evaluation of polynomials, Proceedings of the 2006 ACM symposium on Applied computing , SAC '06, pp.1328-1332, 2006.
DOI : 10.1145/1141277.1141586
URL : https://hal.archives-ouvertes.fr/inria-00000892

R. Bibliography and . Boulton, Boyer-moore automation for the HOL system, Proc. 5th Int. Workshop on Higher Order Logic Theorem Proving and its Applications, volume A-20 of IFIP Transactions, pp.133-142, 1992.

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

R. Boyer and J. Moore, A computational logic handbook, PERSPEC: Perspectives in Computing, vol.23, issue.2, 1988.

R. Boyer, E. Lusk, W. Mccune, R. Overbeek, M. Stickel et al., Set theory in first-order logic: Clauses for G??del's axioms, Journal of Automated Reasoning, vol.2, issue.3, pp.287-327, 1986.
DOI : 10.1007/BF02328452

A. Bundy, A science of reasoning, pp.178-198, 1991.

G. Burel and C. Kirchner, Unbounded Proof-Length Speed-Up in Deduction Modulo, 2007.
DOI : 10.1007/978-3-540-74915-8_37
URL : https://hal.archives-ouvertes.fr/inria-00138195

A. Buronni, Théorie des catégories, p.58, 2004.

H. Cirstea, C. Kirchner, and L. Liquori, Rewrite Strategies in the Rewriting Calculus, Proc. 3rd Int. Workshop on Reduction Strategies in Rewriting and Programming, p.144, 2003.
DOI : 10.1016/S1571-0661(05)82613-1
URL : https://hal.archives-ouvertes.fr/inria-00099586

M. Clavel and J. Meseguer, Reflection and strategies in rewriting logic, Proc. 1st Int. Workshop on Rewriting Logic and its Applications, pp.125-147, 1996.

C. Sacerdoti-coen, E. Tassi, and S. Zacchiroli, Tinycals: Step by Step Tacticals, Electronic Notes in Theoretical Computer Science, vol.174, issue.2, pp.125-142, 2007.
DOI : 10.1016/j.entcs.2006.09.026

R. Constable, S. Allen, M. Bromley, R. Cleaveland, J. Cremer et al., Implementing mathematics with the Nuprl proof development system, 1986.

T. Coquand and G. Huet, Constructions: A higher order proof system for mechanizing mathematics, Proc. European Conf. on Computer Algebra, pp.151-184, 1985.
DOI : 10.1007/3-540-15983-5_13
URL : https://hal.archives-ouvertes.fr/inria-00076155

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, p.143, 2007.
DOI : 10.1007/978-3-540-73228-0_9

E. Crank and M. Felleisen, Parameter-passing and the lambda calculus, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '91, pp.233-244, 1991.
DOI : 10.1145/99583.99616

T. Crolard, Subtractive logic, Theoretical Computer Science, vol.254, issue.1-2, p.124, 2001.
DOI : 10.1016/S0304-3975(99)00124-3
URL : https://hal.archives-ouvertes.fr/hal-00094589

P. Curien and H. Herbelin, The duality of computation, ACM sigplan notices, vol.35, issue.18, p.19, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

V. Danos and C. Laneve, Formal molecular biology, Theoretical Computer Science, vol.325, issue.1, pp.69-110, 2004.
DOI : 10.1016/j.tcs.2004.03.065
URL : https://hal.archives-ouvertes.fr/hal-00164591

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Proc. 14th Int. Conf. on Theorem Proving in Higher Order Logics, pp.169-184, 2001.
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285

. Nicolaas-de-bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions, Proc. of Symp. on Automatic Demonstration, pp.29-61
DOI : 10.1007/BFb0060623

C. Michel-de, The Practice of Everyday Life, 1948.

D. Delahaye, Conception de Langages pour Décrire les Preuves et les Automatisations dans les Outils d'Aidè a la Preuve, Thèse de doctorat, 2001.

D. Delahaye, A Tactic Language for the System Coq, Proc. 7th Int. Conf. on Logic for Programming and Automated Reasoning, pp.85-95, 2000.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070

E. Denney, A Prototype Proof Translator from HOL to Coq, Proc. 13th Int. Conf. on Theorem Proving in Higher Order Logics, pp.108-125, 2000.
DOI : 10.1007/3-540-44659-1_8

G. Dowek and A. Miquel, Cut elimination for Zermelo's set theory, p.141, 2006.

G. Bibliography, B. Dowek, and . Werner, Arithmetic as a theory modulo, Proc. 16th Int. Conf. on Rewriting Techniques and Applications, pp.423-437, 2005.

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.21-45, 2001.
DOI : 10.1017/S0960129500003236
URL : https://hal.archives-ouvertes.fr/inria-00098847

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

C. Dubois, Proving ML Type Soundness Within Coq, Proc. 13th Int. Conf. on Theorem Proving in Higher Order Logics, pp.126-144, 2000.
DOI : 10.1007/3-540-44659-1_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.7996

C. Dubois and O. Boite, Proving type soundness of a simply typed ML-like language with references, Proc. 14th Int. Conf. on Theorem Proving in Higher Order Logics, pp.69-84, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01124763

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol.475, issue.03, pp.795-807, 1992.
DOI : 10.1007/3-540-54487-9_58

S. Eker, M. Knapp, K. Laderoute, P. Lincoln, and C. Talcott, Pathway Logic: Executable Models of Biological Networks, Electronic Notes in Theoretical Computer Science, vol.71, issue.1, p.71, 2002.
DOI : 10.1016/S1571-0661(05)82533-2

J. Filliâtre, Proof of Imperative Programs in Type Theory, Proc. 1998 Int. Conference on Proofs and Programs, p.39, 1998.
DOI : 10.1007/3-540-48167-2_6

G. Gentzen, UntersuchungenüberUntersuchungen¨Untersuchungenüber das logisches schließen, Mathematische Zeitschrift, vol.1, issue.9, pp.176-210, 1935.
DOI : 10.1007/bf01201353

P. Gluck and G. Holzmann, Using SPIN model checking for flight software verification, Proceedings, IEEE Aerospace Conference, 2001.
DOI : 10.1109/AERO.2002.1036832

K. Gödel, Uber die lange von beweisen, Ergebnisse Eines Math. Koll, vol.7, pp.23-24, 1936.

K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory, Annals of Mathematics Studies, vol.3, p.126, 1940.

G. Gonthier, A computer-checked proof of the Four Colour Theorem, p.12, 2005.

M. Gordon and T. Melham, Introduction to HOL: A theorem proving environment for higher order logic, 1993.

M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth, A Metalanguage for interactive proof in LCF, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '78
DOI : 10.1145/512760.512773

M. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF: A Mechanized Logic of Computation, Lecture Notes in Computer Science, vol.78, issue.2, 1979.
DOI : 10.1007/3-540-09724-4

T. Hales, Formalizing the Proof of the Kepler Conjecture, Proc. 17th Int. Conf. on Theorem Proving in Higher Order Logics, pp.117-129, 2004.
DOI : 10.1007/978-3-540-30142-4_9

J. Hannan and D. Miller, From operational semantics to abstract machines, Mathematical Structures in Computer Science, vol.247, issue.04, pp.415-459, 1992.
DOI : 10.1016/0304-3975(75)90017-1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.161.349

T. Hardin, L. Maranget, and B. Pagano, Functional back-ends within the lambda-sigma calculus, Proc. 1st ACM Sigplan Int. Conf. on Functional Programming, pp.25-33, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00073659

S. Hayashi and H. Nakano, PX, a Computational Logic. Foundations of Computing, p.30, 1988.

H. Herbelin, Séquents qu'on Calcule, p.17, 1995.

H. Herbelin, C'est maintenant qu'on calcule, HabilitationàHabilitationà Diriger les Recherches, p.143, 2005.

A. Heyting, Die formalen reglen der intuitionistischen logik, pp.42-56, 1930.

D. Howe, Importing mathematics from HOL into Nuprl, Proc. 9th Int. Conf. on Theorem Proving in Higher Order Logics, pp.267-282, 1996.
DOI : 10.1007/BFb0105410
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.124.4488

I. Johansson, Der minimalkalkül, ein reduzierter intuitionistischer formalismus, Compositio Mathematica, vol.4, pp.119-136, 1937.

J. Bibliography-gueorgui, Holes with binding power, Proc. 2002 Int. Conference on Proofs and Programs, p.31, 2003.

G. Jojgov, Tactics and Parameters, Electronic Notes in Theoretical Computer Science, vol.85, issue.7, p.55, 2003.
DOI : 10.1016/S1571-0661(04)80757-6

G. Jojgov, Incomplete proofs and terms and their use in interactive theorem proving, p.69, 2004.

F. Kirchner, A Finite First-Order Theory of Classes, Proc. 2006 Int. Conference on Proofs and Programs, 2007.
DOI : 10.1007/978-3-540-74464-1_13

F. Kirchner, PVS#: A streamlined tactical language, National Institute of Aerospace, issue.5, 2005.

F. Kirchner, Store-based operational semantics, InSeizì emes Journées Francophones des Langages Applicatifs. Institut National de Recherche en Informatique et en Automatique, 2005.

F. Kirchner and C. Muñoz, PVS#: Streamlined Tacticals for PVS, Proc. 6th Int. Workshop on Strategies in Automated Deduction, pp.47-58
DOI : 10.1016/j.entcs.2006.10.057

F. Kirchner and C. Sacerdoti-coen, The Fellowship proof manager. www.lix.polytechnique.fr/Labo/Florent, 2007.

F. Kirchner and F. Sinot, Rule-Based Operational Semantics for an Imperative Language, Proc. 7th Int. Workshop on Rule Based Programming, pp.35-47, 2005.
DOI : 10.1016/j.entcs.2006.10.023

J. Krivine, Lambda-calculus, Types and Models. Ellis Horwood, 1993. Translated from the 1990 French original by René Cori
URL : https://hal.archives-ouvertes.fr/cel-00574575

S. Lengrand, Normalisation & Equivalence in Proof Theory & Type Theory, p.31, 2006.
URL : https://hal.archives-ouvertes.fr/tel-00134646

S. Lengrand and A. Miquel, A classical version of F ?, Proc. 1st Workshop on Classical logic and Computation, p.143, 2006.

S. Lengrand, R. Dyckhoff, and J. Mckinna, A Sequent Calculus for Type Theory, Proc. 15th Conf. for Computer Science Logic, pp.441-455, 2006.
DOI : 10.1007/11874683_29
URL : https://hal.archives-ouvertes.fr/hal-00150286

X. Leroy, D. Doligez, and J. Garrigue, Didier Rémy, and Jérôme Vouillon) The Objective Caml system, Documentation and user's manual, release 3, p.71, 2003.

H. Lowe and D. Duncan, XBarnacle: Making theorem provers more accessible, Proc. 14th Int. Conf. on Automated Deduction, pp.404-407, 1997.
DOI : 10.1007/3-540-63104-6_39
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.297

L. Magnusson, The Implementation of ALF: A Proof Editor Based on Martin-Löf 's Monomorphic Type Theory with Explicit Substitution, p.31, 1995.

A. Martin and J. Gibbons, A monadic interpretation of tactics, p.69, 2002.

A. Martin, P. Gardiner, and J. Woodcock, A tactic calculus, Formal Aspects of Computing, p.55, 1996.

M. Mayero, Formalisation et Automatisation de Preuves en Analyses Réelle et numérique, p.139, 2001.

C. Mcbride, Epigram: Practical Programming with Dependent Types, Advanced Functional Programming, pp.130-170
DOI : 10.1007/11546382_3

N. Megill, A Finitely Axiomatized Formalization of Predicate Calculus with Equality, Notre Dame Journal of Formal Logic, vol.36, issue.3, pp.435-453, 0141.
DOI : 10.1305/ndjfl/1040149359

E. Mendelson, Introduction to Mathematical Logic, p.140, 1997.
DOI : 10.1007/978-1-4615-7288-6

J. Meseguer and G. Ro¸suro¸su, The rewriting logic semantics project, Theoretical Computer Science, p.50, 2006.

E. Moggi, Computational lambda-calculus and monads Logic in Computer Science, Proc. 4th IEEE Symp, p.58, 1989.

E. Bibliography and . Moggi, Notions of computation and monads. Information and Computation, pp.55-92, 1991.

C. Muñoz, Un calcul de substitutions pour la représentation de preuves partielles en théorie de types, Thèse de doctorat, p.33, 1997.

C. Muñoz, Proof-term synthesis on dependent-type systems via explicit substitutions, Theoretical Computer Science, vol.266, issue.1-2, pp.407-440, 2001.
DOI : 10.1016/S0304-3975(00)00196-1

C. Muñoz, Dependent types and explicit substitutions: a meta-theoretical development, Mathematical Structures in Computer Science, vol.11, issue.1, pp.91-129, 2001.
DOI : 10.1017/S0960129500003261

C. Muñoz and M. Mayero, Real automation in the field, p.139, 2001.

P. Naumov, M. Stehr, and J. Meseguer, The HOL/NuPRL Proof Translator, Proc. 14th Int. Conf. on Theorem Proving in Higher Order Logics, pp.329-345, 2001.
DOI : 10.1007/3-540-44755-5_23

T. Nipkow and . Jinja, Towards a comprehensive formal semantics for a Java-like language, Proc. Marktobderdorf Summer School, p.35, 2003.

T. Nipkow, Winskel is (almost) Right: Towards a Mechanized Semantics Textbook, Formal Aspects of Computing, vol.10, issue.2, pp.171-186, 1998.
DOI : 10.1007/s001650050009
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.9270

S. Obua and S. Skalberg, Importing HOL into Isabelle/HOL, Proc. 3rd Int. Joint Conf. on Automated Reasoning, pp.298-302, 2006.
DOI : 10.1007/11814771_27

S. Owre and N. Shankar, The formal semantics of PVS, p.101, 1999.

S. Owre, J. Rushby, and N. Shankar, PVS: A prototype verification system, Proc. 11th Int. Conf. on Automated Deduction, pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.2627

C. Paulin-mohring, Inductive definitions in the system Coq rules and properties, Proc. 1st Int. Conf. on Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pp.328-345, 1993.
DOI : 10.1007/BFb0037116

L. Paulson, Experience with isabelle : A generic theorem prover, 1988.
DOI : 10.1007/bf00248324
URL : http://arxiv.org/abs/cs/9301105

L. Paulson, Set theory for verification: I. From foundations to functions, Journal of Automated Reasoning, vol.8, issue.1, pp.353-389, 1993.
DOI : 10.1007/BF00881873
URL : http://arxiv.org/abs/cs/9311103

L. Pinto and R. Dyckhoff, Sequent calculi for the normal terms of the ??-and ???-calculi, Proc. Workshop on Proof Search in Type-Theoretic Languages, p.143, 1998.

A. Pitts, Operational Semantics and Program Equivalence, Applied Semantics, Advanced Lectures, pp.378-412, 2002.
DOI : 10.1007/3-540-45699-6_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.166

G. Plotkin, A structural approach to operational semantics, p.35, 1981.

R. Pollack, The Theory of Lego: A Proof Checker for the Extended Calculus of Constructions, 1994.

F. Pottier and D. Rémy, The essence of ML type inference, Advanced Topics in Types and Programming Languages, pp.389-489, 2005.

D. Prawitz, Natural Deduction: a Proof-Theoretical Study, Stockholm Studies in Philosophy. Almqvist & Wiksell, vol.3, p.93, 1965.

A. Quaife, Automated deduction in von Neumann-Bernays-Gödel set theory, Journal of Automated Reasoning, vol.8, issue.1, pp.91-147, 1992.

C. Rauszer, Semi-boolean algebras and their applications to intuitionistic logic with dual operations, Fundamenta Mathematicae, vol.83, issue.3, pp.219-249, 1974.

T. Ridge and J. Margetson, A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic, Proc. 18th Int. Conf. on Theorem Proving in Higher Order Logics, pp.294-309
DOI : 10.1007/11541868_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.580

J. M. Rushby, Harnessing Disruptive Innovation in Formal Verification, Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06), pp.21-30, 2006.
DOI : 10.1109/SEFM.2006.24

. Bibliography-claudio-sacerdoti-coen, Explanation in natural language of ¯ ?µ?µ?µ?µ-terms, Proc. 4th Int. Conf. on Mathematical Knowledge Management, pp.234-249, 2006.

A. Saurin, Focussing as proof normalization, 2006.

H. Schwichtenberg, Minimal Logic for Computable Functions, Logic and Algebra of Specification, volume 94 of Series F: Computer and Systems Sciences, pp.289-320, 1993.
DOI : 10.1007/978-3-642-58041-3_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.3511

P. Severi and E. Poll, Pure Type Systems with definitions, Proc. 3rd Int. Symp. on Logical Foundations of Computer Science, pp.316-328, 1994.
DOI : 10.1007/3-540-58140-5_30
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.1076

A. Trybulec, The Mizar-QC/6000 logic information language, Association for Literary and Linguistic Computing Bulletin, pp.136-140, 1978.

C. Urban, Strong Normalisation for a Gentzen-like Cut-Elimination Procedure, Proc. 5th Int. Conf. on Typed Lambda Calculi and Applications, pp.415-429, 2001.
DOI : 10.1007/3-540-45413-6_32

C. Urban and G. Bierman, Strong normalisation of cutelimination in classical logic, Proc. 4th Int. Conf. on Typed Lambda Calculi and Applications, pp.365-380, 1999.

S. Vaillant, A Finite First-Order Presentation of Set Theory, Proc. 2002 Int. Conference on Proofs and Programs, pp.316-330, 2002.
DOI : 10.1007/3-540-39185-1_18
URL : https://hal.archives-ouvertes.fr/inria-00072244

E. Visser and . Stratego, Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5, Proc. 12th Int. Conf. on Rewriting Techniques and Applications, pp.357-362, 2001.
DOI : 10.1007/3-540-45127-7_27

. John-von-neumann, Eine axiomatisierung der mengenlehre, Journal für die reine und angewandte Mathematik, vol.154, pp.219-240, 1925.

P. Wadler, Call-by-value is dual to call-by-name, ACM SIGPLAN Notices, vol.38, issue.9, pp.189-201, 2003.
DOI : 10.1145/944746.944723

P. Wadler, Monads for functional programming, Advanced Functional Programming, p.61, 1995.
DOI : 10.1007/3-540-59451-5_2
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.9674

D. Wasserrab, T. Nipkow, G. Snelting, and F. Tip, An operational semantics and type safety proof for multiple inheritance in C++, OOPSLA '06: Object oriented programming, systems, languages, and applications, p.36, 2006.

F. Wiedijk, The Seventeen Provers of the World, Lecture Notes in Artificial Intelligence, vol.3600, issue.2, 2006.
DOI : 10.1007/11542384

G. Winskel, The Formal Semantics of Programming Languages. Foundations of Computing WIN g2 93:1 P-Ex, p.44, 1993.

A. Wright and M. Felleisen, A syntactic approach to type soundness . Information and Computation, pp.38-94, 1994.
DOI : 10.1006/inco.1994.1093
URL : http://doi.org/10.1006/inco.1994.1093