Y. Andou, Church???Rosser property of a simple reduction for full first-order classical natural deduction, Annals of Pure and Applied Logic, vol.119, issue.1-3, pp.225-237, 2003.
DOI : 10.1016/S0168-0072(02)00051-9

Y. Andou, A normalization-procedure for the first order classical natural deduction with full logical symbols, Tsukuba J. Math, vol.19, pp.153-162, 1995.

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 the strong normalization results for the symmetric ?µcalculus, TLCA'05, pp.162-178, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00382299

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-111, 2005.
DOI : 10.1016/j.entcs.2005.06.020
URL : https://hal.archives-ouvertes.fr/hal-00382686

D. Groote, On the Strong Normalization of Natural Deduction with Permutation-Conversions, RTA'99, pp.45-59, 2005.
DOI : 10.1007/3-540-48685-2_4

D. Groote, Strong Normalization of Classical Natural Deduction with Disjunction, TLCA'01, pp.182-196, 2001.
DOI : 10.1007/3-540-45413-6_17

G. Gentzen, Recherches sur la déduction logique, 1955.

R. Matthes, Non-strictly positive fixed points for classical natural deduction, Annals of Pure and Applied Logic, vol.133, issue.1-3, pp.205-230, 2005.
DOI : 10.1016/j.apal.2004.10.009
URL : http://doi.org/10.1016/j.apal.2004.10.009

K. Nakazawa, Confluency and strong normalizability of call-by-value ????-calculus, Theoretical Computer Science, vol.290, issue.1, pp.429-463, 2003.
DOI : 10.1016/S0304-3975(01)00380-2

K. Nour and K. Saber, A semantical proof of the strong normalization theorem for full propositional classical natural deduction, Archive for Mathematical Logic, vol.45, issue.3, pp.357-364, 2005.
DOI : 10.1007/s00153-005-0314-y
URL : https://hal.archives-ouvertes.fr/hal-00380651

K. Nour and K. Saber, Some properties of full propositional classical natural deduction, 2006.

C. L. Ong and C. A. Stewart, A Curry-Howard foundation for functional computation with control, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, pp.215-227, 2001.
DOI : 10.1145/263699.263722

M. Parigot, ?µ-calculus: An algorithm interpretation of classical natural deduction, Lecture Notes in Artificial Intelligence, vol.624, pp.190-201, 1992.

D. Prawitz, Natural deduction-A Proof Theoretical Study, Almqvist & Wiksell, 1965.

D. Prawitz, Idea and result in proof theory, 2nd Scandinavian Logic Symp, pp.235-307, 1971.

W. Py, Confluence en ?µ-calcul, 1998.

E. Ritter and D. Pym, On the semantic of classical disjunction, Journal of Pure and Applied Algebra, vol.159, pp.315-338, 2001.

E. Ritter, D. Pym, and L. Wallen, On the intuitionistic force of classical search, Theoretical Computer Science, vol.232, issue.1-2, pp.299-333, 2000.
DOI : 10.1016/S0304-3975(99)00178-4

E. Ritter, D. Pym, and L. Wallen, Proof-terms for classical and intuitionistic resolution, Journal of Logic and Computation, vol.10, issue.2, pp.173-207, 2000.
DOI : 10.1093/logcom/10.2.173