H. P. Barendregt, M. Coppo, and M. Dezani-ciancaglini, A lter lambda model and the completeness of type assignment, Journal of Symbolic Logic, vol.48, pp.931-940, 1983.

P. N. B-e-n-ton, Strictness Analysis of Lazy Functional Programs, 1992.

S. Berardi, Pruning Simply Typed Lambda Terms, Journal of Logic and Computation, vol.6, issue.5, pp.663-681, 1996.

S. Berardi and L. Boerio, Using Subtyping in Program Optimization, Typed L ambda Calculus and Applications, pp.1-9

L. Boerio, Optimizing Programs Extracted f r om Proofs, 1995.

C. and P. Ohring, Extracting F!'s Programs from Proofs in the Calculus of Constructions, POPL'89. A CM, 1989.

C. and P. Ohring, Extraction des Programmes dans le Calcul des Constructions, 1989.

G. Castagna, Covariance and contravariance: connict without a cause, ACM Transactions on Programming Languages and Systems, vol.17, issue.3, pp.431-447, 1995.

G. Castagna, Object-Oriented P r ogramming: A Uniied F oundation, Progress in Theoretical Computer Science. Birkk auser, 1996.

M. Coppo, F. Damiani, and P. Giannini, Reenement T ypes for Program Analysis, SAS'96, vol.1145, pp.143-158, 1996.

M. Coppo and M. Dezani-ciancaglini, An extension of basic functional theory for lambdacalculus, Notre Dame Journal of Formal Logic, vol.21, issue.4, pp.685-693, 1980.

M. Coppo and A. Ferrari, Type inference, abstract interpretation and strictness analysis, Theoretical Computer Science, vol.121, pp.113-145, 1993.

D. Dussart, F. Henglein, and C. Mossin, Polymorphic Recursion and Subtype Qualiications: Polymorphic Binding-Time Analysis in Polynomial Time, SAS'95, vol.983, pp.118-135, 1995.

F. Damiani and P. Giannini, An Inference Algorithm for Strictness, TLCA'97, 1997.

C. Hankin and D. Le-m-etayer, Deriving algorithms for type inference systems: Applications to strictness analysis, POPL'94, pp.202-212, 1994.

T. P. Jensen, Abstract Interpretation in Logical Form, 1992.

G. Kahn, Programming Of Future Generation Computer, 1988.

T. M. Kuo and P. Mishra, Strictness analysis: a new perspective b a s e d o n t ype inference, Functional Programming Languages and Computer Architecture, pp.260-272, 1989.

J. Palsberg and P. O'keefe, A Type System Equivalent t o F l o w Analysis, POPL'95, pp.367-378, 1995.

A. M. Pitts, Summer School on Semantics and Logics of Computation, pp.25-29, 1995.

F. Prost, Marking techniques for extraction, 1995.
URL : https://hal.archives-ouvertes.fr/hal-02102062

K. L. Solberg, Annotated T ype Systems for Program Analysis, Aarhus University, 1995.

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

S. Van-bakel, Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems, 1993.

D. A. Wright, Reduction Types and Intensionality in the Lambda-Calculus, 1992.