A. Armando, M. Rusinowitch, and S. Stratulat, Incorporating Decision Procedures in Implicit Induction, Journal of Symbolic Computation, vol.34, issue.4, pp.241-258, 2002.
DOI : 10.1006/jsco.2002.0549
URL : https://hal.archives-ouvertes.fr/inria-00100610

G. Barthe and S. Stratulat, Validation of the JavaCard Platform with Implicit Induction Techniques, Lecture Notes in Computer Science, vol.2706, pp.337-351, 2003.
DOI : 10.1007/3-540-44881-0_24

A. Bouhoula, E. Kounalis, and M. Rusinowitch, Automated Mathematical Induction, Journal of Logic and Computation, vol.5, issue.5, pp.631-668, 1995.
DOI : 10.1093/logcom/5.5.631
URL : https://hal.archives-ouvertes.fr/inria-00074484

R. Boulton and K. Slind, Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions, Computational Logic ? CL, pp.629-643, 2000.
DOI : 10.1007/3-540-44957-4_42

R. S. Boyer and J. S. Moore, A computational logic handbook, 1988.

R. S. Boyer and J. S. Moore, Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic, 1988.

R. M. Burstall, Proving Properties of Programs by Structural Induction, The Computer Journal, vol.12, issue.1, pp.41-48, 1969.
DOI : 10.1093/comjnl/12.1.41

E. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain, Certification of Automated Termination Proofs, Frontiers of Combining Systems, pp.148-162, 2007.
DOI : 10.1007/978-3-540-74621-8_10
URL : https://hal.archives-ouvertes.fr/hal-01125312

J. Courant, Proof reconstruction, 1996.

D. Delahaye, A Tactic Language for the System Coq, Logic for Programming and Automated Reasoning (LPAR), pp.85-95, 1955.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070

B. Gramlich, Strategic Issues, Problems and Challenges in Inductive Theorem Proving, Electronic Notes in Theoretical Computer Science, vol.125, issue.2, pp.5-43, 2005.
DOI : 10.1016/j.entcs.2005.01.006

D. Kapur and M. Subramaniam, Automating induction over mutually recursive functions, Algebraic Methodology and Software Technology, pp.117-131, 1996.
DOI : 10.1007/BFb0014311

D. E. Knuth and P. B. Bendix, Simple Word Problems in Universal Algebras, Computational Problems in Abstract Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy et al., The Objective Caml system -release 3.12. Documentation and user's manual

D. R. Musser, On proving inductive properties of abstract data types, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '80, pp.154-162, 1980.
DOI : 10.1145/567446.567461

M. Protzen, Lazy generation of induction hypotheses Automated Deduction ? CADE-12, pp.42-56, 1994.

M. Rusinowitch, S. Stratulat, and F. Klay, Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm, J. Autom. Reasoning, vol.30, issue.2, pp.53-177, 2003.
DOI : 10.1007/10722167_27
URL : https://hal.archives-ouvertes.fr/inria-00099167

S. Stratulat, A General Framework to Build Contextual Cover Set Induction Provers, Journal of Symbolic Computation, vol.32, issue.4, pp.403-445, 2001.
DOI : 10.1006/jsco.2000.0469
URL : https://hal.archives-ouvertes.fr/inria-00100927

S. Stratulat, Integrating Implicit Induction Proofs into Certified Proof Environments, Integrated Formal Methods, pp.320-335, 2010.
DOI : 10.1007/978-3-540-70590-1_24
URL : https://hal.archives-ouvertes.fr/hal-00553070

S. Stratulat, A unified view of induction reasoning for first-order logic, EPiC Series, vol.10, pp.326-352, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00763236

S. Stratulat and V. Demange, Automated Certification of Implicit Induction Proofs, CPP'2011 (First International Conference on Certified Programs and Proofs), pp.37-53, 2011.
DOI : 10.1007/978-3-642-16265-7_23
URL : https://hal.archives-ouvertes.fr/hal-00644876

R. Voicu and M. Li, Descente Infinie proofs in Coq, The 1st Coq Workshop, p.12, 2009.

C. Wirth, Descente Infinie + Deduction, Logic Journal of IGPL, vol.12, issue.1, pp.1-96, 2004.
DOI : 10.1093/jigpal/12.1.1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.9.619