D. Baelde, Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, issue.1, 2012.

D. Baelde and K. Chaudhuri, Abella: A System for Reasoning about Relational Specifications, Journal of Formalized Reasoning, vol.7, issue.2, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

D. Baelde and &. Miller, Least and greatest fixed points in linear logic, International Conference on Logic for Programming and Automated Reasoning (LPAR), pp.92-106, 2007.

D. Baelde, D. Miller, and &. Snow, Focused Inductive Theorem Proving, Fifth International Joint Conference on Automated Reasoning, pp.278-292, 2010.
DOI : 10.1007/978-3-642-14203-1_24
URL : https://hal.archives-ouvertes.fr/hal-00772592

A. Bundy, A. Stevens, F. Van-harmelen, A. Ireland, and &. A. Smaill, Rippling: A heuristic for guiding inductive proofs, Artificial Intelligence, vol.62, issue.2, pp.185-25310, 1993.
DOI : 10.1016/0004-3702(93)90079-Q

A. Bundy, The use of explicit plans to guide inductive proofs, Conf. on Automated Deduction (CADE 9), pp.111-120, 1987.
DOI : 10.1007/BFb0012826

Z. Chihani, D. Miller, and &. Renaud, Foundational Proof Certificates in First-Order Logic, Conference on Automated Deduction 2013, LNAI 7898, pp.162-177, 2013.
DOI : 10.1007/978-3-642-38574-2_11
URL : https://hal.archives-ouvertes.fr/hal-00906485

D. Miller and &. Nadathur, Programming with Higher-Order Logic, pp.10-1017, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

F. Pfenning and &. Carsten-schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, 16th Conf. on Automated Deduction (CADE), LNAI 1632, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

C. Schürmann and &. Pfenning, A Coverage Checking Algorithm for LF, Theorem Proving in Higher Order Logics: 16th International Conference TPHOLs 2003, pp.120-135, 2003.
DOI : 10.1007/10930755_8

S. Wilson and J. , Inductive Proof Automation for Coq, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00489496