S. Berardi, L. Boerio, ;. Barras, S. Boutin, C. Cornes et al., The Coq Proof Assistant Reference Manual Version 6, Proceedings of TLCA'95, vol.902, 1995.

S. Berardi, Pruning simply typed ?-terms, 1993.

L. Boerio, Extending pruning techniques to polymorphic second order ?-calculus, Proceedings of ESOP'94, vol.788, pp.120-134, 1994.

P. Cousot and R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL '77 ), pp.238-252, 1977.

D. Clément, J. Despeyroux, T. Desperoux, and G. Kahn, A simple applicative language: Mini-ML, Technical Report, vol.529, 1986.

D. Dussart, F. Henglein, and C. Mossin, Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial, SAS'95: 2nd Int'l Static Analysis Symposium, vol.983, pp.118-135, 1995.

F. Damiani and F. Prost, Detecting and removing dead code using rank-2 intersection, International Workshop:"TYPES'96, vol.1512, 1998.

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, 1989.

N. Heintze, Control-flow analysis and type systems, Proceeding of SAS 1995, vol.983, pp.189-206, 1995.

C. Hankin and D. L. Métayer, A type-based framework for program analysis, Proceedings of the Static Analysis Symposium, vol.864, pp.380-394, 1994.

S. Hunt, Abstract Interpretation of functionnal languages : from theory to Practice, 1991.

Z. Luo and R. Pollack, Lego proof development system : User's manual, 1992.

J. C. Mitchell, A type inference approach to reduction properties and semantics of polymorphic expressions, Logical Foundations of Functionnal programming, pp.195-211, 1990.

H. R. Nielson, K. L. Solberg, and F. Nielson, Strictness and totality analysis, Static Analysis, vol.864, pp.408-422, 1994.

C. Paulin, Extraction de programmes dans le calcul des constructions, 1989.
URL : https://hal.archives-ouvertes.fr/tel-00431825

C. Paulin-mohring, Extracting F?'s programs from proofs in the Calculus of Constructions, Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989.

F. Prost, Using ML type inference for dead code analysis, 1997.

K. and L. Solberg, Annotated Type Systems for Program Analysis, 1995.

J. Talpin and P. Jouvelot, The type and effect discipline, Proceedings of the 1992 Conference on Logic in Computer Science, 1992.

, This article was processed using the L A T E X macro package with LLNCS style