Z. M. Ariola and H. Herbelin, Minimal classical logic and control operators, ICALP: Annual International Colloquium on Automata, Languages and Programming, vol.2719, pp.871-885, 2003.

F. Barbanera and S. Berardi, A symmetric lambda calculus for classical program extraction, Information and Computation, vol.125, issue.2, pp.103-117, 1996.

F. Barbanera, M. Dezani-ciancaglini, and U. De'-liguoro, Intersection and union types: syntax and semantics. Information and Computation, vol.119, pp.202-230, 1995.

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

H. P. Barendregt and S. Ghilezan, Lambda terms for natural deduction, sequent calculus and cut-elimination, Journal of Functional Programming, vol.10, issue.1, pp.121-134, 2000.

G. M. Bierman, A computational interpretation of the ?µ-calculus, Proceedings of Symposium on Mathematical Foundations of Computer Science, vol.1450, pp.336-345, 1998.

P. Buneman and B. Pierce, Union types for semistructured data, Proceedings of the International Database Programming Languages Workshop, vol.1686, 1998.

M. Coppo, M. Dezani-ciancaglini, and B. Venneri, Principal type schemes and ?-calculus semantics, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.535-560, 1980.

P. Curien, Symmetry and interactivity in programming. Archive for Mathematical Logic, 2001.
URL : https://hal.archives-ouvertes.fr/hal-00003868

P. Curien, Abstract machines, control, and sequents, Applied Semantics, International Summer School, APPSEM, vol.2395, pp.123-136, 2000.

P. Curien and H. Herbelin, The duality of computation, Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00), 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

. Ph and . De-groote, On the relation between the ?µ-calculus and the syntactic theory of sequential control, Proceedings of the (th International Conference on Logic Programming and Automated Reasoning, vol.822, pp.31-43, 1994.

J. Girard, A new constrcutive logic: classical logic, Mathematical Structures in Computer Science, vol.1, issue.3, pp.255-296, 1991.

T. Griffin, A formulae-as-types notion of control, Proceedings of the 17th Annual ACM Symposium on Principles Of Programming Languages, pp.47-58, 1990.

H. Herbelin, Séquents qu'on calcule : de l'interprétation du calcul des séquents comme calcul de ?-termes et comme calcul de stratégies gagnantes, 1995.

J. R. Hindley, Coppo-Dezani types do not correspond to propositional logic, Theoretical Computer Science, vol.28, issue.1-2, pp.235-236, 1984.

O. Laurent, On the denotational semantics of the pure lambda-mu calculus, 2004.

S. Lengrand, Call-by-value, call-by-name, and strong normalization for the classical sequent calculus, Electronic Notes in Theoretical Computer Science, vol.86, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00150290

C. L. Ong and C. A. Stewart, A Curry-Howard foundation for functional computation with control, Proceedings of the 24th Annual ACM Symposium on Principles Of Programming Languages, pp.215-227, 1997.

J. Palsberg and C. Pavlopoulou, From polyvariant flow information to intersection and union types, J. Funct. Programming, vol.11, issue.3, pp.263-317, 2001.

M. Parigot, An algorithmic interpretation of classical natural deduction, Proc. of Int. Conf. on Logic Programming and Automated Reasoning, LPAR'92, pp.190-201, 1992.

M. Parigot, Proofs of strong normalisation for second order classical natural deduction, The Journal of Symbolic Logic, vol.62, issue.4, pp.1461-1479, 1997.

B. C. Pierce, Programming with intersection types, union types, and polymorphism, 1991.

E. Polonovski, Strong normalization of ?µ?µ?µ?µ-calculus with explicit substitutions, Foundations of Software Science and Computation Structures, 7th International Conference, vol.2987, pp.423-437, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00004321

G. Pottinger, Normalization as homomorphic image of cut-elimination, Annals of Mathematical Logic, vol.12, pp.323-357, 1977.

G. Pottinger, A type assignment for the strongly normalizable ?-terms, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.561-577, 1980.

J. C. Reynolds, Design of the programming language Forsythe, 1996.

C. Urban and G. M. Bierman, Strong normalisation of cut-elimination in classical logic, Typed Lambda Calculus and Applications, vol.1581, pp.365-380, 1999.

P. Wadler, Call-by-value is dual to call-by-name, Proceedings of the 8th International Conference on Functional Programming, 2003.

J. B. Wells, A. Dimock, R. Muller, and F. Turbak, A calculus with polymorphic and polyvariant flow types, J. Funct. Programming, vol.12, issue.3, pp.183-227, 2002.