, To all those people I can just say thank you and try to pay them back with words and remarks which will (i hope) bring them the spark they look for, just as they have done for me. I also would like to thank M. Gengler for his very deep and helpful proofreading

S. Berardi, Pruning Simply -terms, 1993.

L. Boerio, Extending Pruning Techniques to Polymorphic Second Order -Calculus

S. Berardi and L. Boerio, Using Subtyping in Program Optimization, Lectures Note in Computer Science, vol.902, 1995.

R. L. Constable, Implementing Mthematics with the Nuprl Proo Development System, 1986.

C. Cornes, The Coq Proo Assistant Reference Manual, 1995.

J. and G. , Interpr etation fonctionnelle et elimination des coupures de l'arithm etique d'ordre sup erieur, 1972.

C. Goad, Proofs as description of computation, Proc. of the 5 th Conference on Automated Deduction, Les Arcs, vol.87, 1980.

G. Huet, A uniform approach to type t h e ory. Logical foudations of functionnal programing, 1990.

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

C. Paulin, Informative contents as annotations in the Calculus of Inductive Constructions, 1995.

Y. Takayama, Extraction of Redundancy-free P r ograms from Constructive Natural Deduction Proofs, Journal of Symbolic Computation, vol.12, pp.29-69, 1991.