F. Barbanera and S. Berardi, A symmetric lambda-calculus for classical program extraction, TACS'94, pp.495-515, 1994.

H. Barendregt, The lambda calculus -Its syntax and semantics, 1984.

A. Church, The calculi of lambda conversion, 1941.

P. Curien and H. Herbelin, The duality of computation, International Conference on Functional Programming, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

H. Curry and R. Feys, Combinatory logic, 1958.

H. Curry, J. Hindley, and J. Seldin, Combinatory logic, 1972.

R. David and K. Nour, Why the Usual Candidates of Reducibility Do Not Work for the Symmetric ????-calculus, Electronic Notes in Theoretical Computer Science, vol.140, pp.101-112, 2005.
DOI : 10.1016/j.entcs.2005.06.020
URL : https://hal.archives-ouvertes.fr/hal-00382686

R. David and K. Nour, A short proof of the strong normalization of the simply typed ?µ-calculus, Schedae Informaticae, vol.12, pp.27-34, 2003.
URL : https://hal.archives-ouvertes.fr/hal-00382688

R. David and K. Nour, Abstract, The Journal of Symbolic Logic, vol.51, issue.04, pp.1277-1288, 2003.
DOI : 10.1093/logcom/10.2.173

R. David and K. Nour, Arithmetical proofs of strong normalization results for symmetric ?-calculi, Fundamenta Informaticae
URL : https://hal.archives-ouvertes.fr/hal-00381602

R. David and K. Nour, Arithmetical proofs of the strong normalization results for the symmetric ?µcalculus, TLCA'05, pp.162-178, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00382299

P. Degroote, A cps-translation of the lambda-mu-calculu, CAAP'94, pp.85-99, 1994.

P. Degroote, A simple calculus of exception handling, TLCA'95, pp.201-215, 1995.

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, vol.7, issue.2, pp.255-296, 1991.
DOI : 10.1016/0304-3975(87)90045-4

J. Hindley and J. Seldin, Introduction to combinators and the lambda calculus, 1986.
DOI : 10.1017/CBO9780511809835

J. Hindley, B. Lercher, and J. Seldin, Introduction to combinatory logic, 1972.

M. Holmes, Systems of combinatory logic related to Quine's ???New Foundations???, Annals of Pure and Applied Logic, vol.53, issue.2, pp.103-133, 1991.
DOI : 10.1016/0168-0072(91)90052-N

J. Krivine, Classical logic, storage operators and second-order lambda-calculus, Annals of Pure and Applied Logic, vol.68, issue.1, pp.53-78, 1994.
DOI : 10.1016/0168-0072(94)90047-7
URL : http://doi.org/10.1016/0168-0072(94)90047-7

B. Lercher, Strong reduction and normal form in combinatory logic, The Journal of Symbolic Logic, vol.32, issue.02, pp.213-223, 1967.
DOI : 10.1305/ndjfl/1093957876

M. Parigot, Free deduction: An analysis of ???Computations??? in classical logic, Logic Progr. and Autom. Reasoning, pp.361-380, 1991.
DOI : 10.1007/3-540-55460-2_27

M. Parigot, ?µ-calculus: an algorithm interpretation of classical natural deduction, LPAR'92, pp.190-201, 1992.

N. Rehof and M. Sorensen, The ? ? -calculus, TACS'94, pp.516-542, 1994.

M. Schönfinkel, ???ber die Bausteine der mathematischen Logik, Mathematische Annalen, vol.92, issue.3-4, pp.305-316, 1924.
DOI : 10.1007/BF01448013

P. Wadler, Call-by-value is dual to call-by-name. re-loaded, RTA'05, pp.185-203, 2005.

P. Wadler, Call-by-value is dual to call-by-name, International Conference on Functional Programming, 2003.
DOI : 10.1145/944705.944723