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

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

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. Berger, F. Bonomi, and K. Fendick, Proposed TM baseline text on an ABR conformance definition, 1995.

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

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

C. Kaliszyk, Validation des preuves par récurrence implicite avec des outils basés sur le calcul des constructions inductives, 2005.

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.
DOI : 10.1145/1743546.1743574

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

F. Nahon, C. Kirchner, H. Kirchner, and P. Brauner, Inductive proof search modulo, Annals of Mathematics and Artificial Intelligence, vol.28, issue.6, pp.123-154, 2009.
DOI : 10.1007/s10472-009-9154-5
URL : https://hal.archives-ouvertes.fr/inria-00337380

C. Rabadan and F. Klay, Un nouvel algorithme de contrôle de conformité pour la capacité de transfert 'Available Bit Rate, 1997.

M. Rusinowitch, S. Stratulat, and F. Klay, Mechanical verification of a generic incremental ABR conformance algorithm, 1999.
URL : https://hal.archives-ouvertes.fr/inria-00099017

M. Rusinowitch, S. Stratulat, and F. Klay, Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm, Lecture Notes in Computer Science, vol.1855, pp.344-357, 2000.
DOI : 10.1007/10722167_27
URL : https://hal.archives-ouvertes.fr/inria-00099167

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, Automatic ???Descente Infinie??? Induction Reasoning, Lecture Notes in Artificial Intelligence, vol.3702, pp.262-276, 2005.
DOI : 10.1007/11554554_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.614.3669

S. Stratulat, 'Descente Infinie' Induction-Based Saturation Procedures, Ninth International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2007), pp.17-24, 2007.
DOI : 10.1109/SYNASC.2007.17

S. Stratulat, Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities, Rewriting Techniques and Applications, pp.351-365, 2008.
DOI : 10.1007/978-3-540-70590-1_24

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 and V. Demange, Validating implicit induction proofs using certified proof environments. Poster session of 2010 Grande Region Security and Reliability Day, 2010.
DOI : 10.1007/978-3-642-16265-7_23
URL : https://hal.archives-ouvertes.fr/hal-00553070/document