Y. Bertot and &. Pierre-castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Blanqui and J. Strub, From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures, pp.349-365, 2008.
DOI : 10.1007/978-0-387-09680-3_24
URL : https://hal.archives-ouvertes.fr/inria-00275382

C. Cornes and &. Terrasse, Automating inversion of inductive predicates in Coq, pp.85-104, 1995.
DOI : 10.1007/3-540-61780-9_64

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

C. Mcbride, Inverting inductively defined relations in LEGO, TYPES, Lecture Notes in Computer Science 1512, pp.236-253, 1996.
DOI : 10.1007/BFb0097795

J. Mckinna, Why dependent types matter, ACM SIGPLAN Notices, vol.41, issue.1, pp.1-1, 2006.
DOI : 10.1145/1111320.1111038

H. Nielson, Semantics with applications: a formal introduction, 1992.

C. Benjamin, C. Pierce, &. Casinghino, and . Greenberg, Software Foundations, 2009.