LINK [1] H. P. Barendregt, “Lambda calculi with types,”In Hand book of Logic in Computer Science, vol. 2, S. Abramsky et al., Eds., Oxford University Press, pp.118-309, 1992.

LINK [2] R. David and K. Nour, “A short proof of the strong normalization of classical natural deduction with disjunction,”Journal of Symbolic Logic, vol. 68, no. 4, pp.1277-1288, 2003.

LINK [3] P. de Groote, “On the Strong Normalisation of Intuitionistic Natural Deduction with Permutative-Conversions,”Inf. Comput. vol. 178, pp.441-464, 2002.

LINK [4] J. H. Gallier, On Girard’s “Candidats de reducibilite” In Logic and Computer Science, P. Odifreddi, Ed., Academic Press, pp.123-203, 1990.

LINK [5] J. Y. Girard, “Une extension de l’nterpréation de Gödel à ’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types,“In Proc. of the Second Scandinavian Logic Symposium, J. E. Fenstad, Ed., North-Holland, pp.63-92, 1971.

LINK [6] J. Y. Girard, “Interprétation fonctionelle et élimination des coupures de l’arithmétique d´ordre supérieur,“Thése de Doctorat d´Etat, Université de Paris VII, 1972.

LINK [7] J. Y. Girard, P. Taylor, and Y. Lafont, Proofs And Types, Cambridge University Press, 1989.

LINK [8] W. A. Howard, “The formulae-as-types notion of construction,” In To H. B. Curry : essays on combinatory logic, lambda calculus and formalism, J. P. Seldin and J. R. Hindley, Eds., Academic Press, pp.480-490, 1980.

LINK [9] F. Joachimski and R. Matthes, “Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel’s T,” Archive for Mathematical Logic, vol. 42, pp.59-87, 2003.

LINK [10] D. Leivant, “Strong normalization for arithmetic,” Lecture Notes in Mathematics, vol, 500, pp.182-197, 1975.

LINK [11] P. Martin-Löf, “Hauptsatz for the theory of species,” In Proc. of the Second Scandinavian Logic Symposium, J. E. Fenstad, Ed., North-Holland, pp.217-233, 1971.

LINK [12] R. Matthes, “Non-Strictly Positive Fixed-Points for Classical Natural Deduction,” Annals of Pure and Applied Logic, vol. 133, pp.205-230, 2005.

LINK [13] J. C. Mitchell and G. Plotkin, “Abstract types have existential type,” ACM Transactions on Programming Languages and Systems, vol. 10, no. 3, pp.470-502, 1988.

LINK [14] D. Prawitz, Natural Deduction, Almquist and Wiksell, 1965.

LINK [15] D. Prawitz, “Ideas and results of proof theory,” In Proc. Second Scandinavian Logic Symposium, J. E. Fenstad, Ed. North-Holland, pp.235-307, 1971.

LINK [16] J. C. Reynolds, “Towards a Theory of Type Structure,” Lecture Notes in Computer Science, vol. 19, pp.408-425, 1974.

LINK [17] W. W. Tait, “A realizability interpretation of the theory of species,” Lecture Notes in Mathematics, vol. 453, pp.240-251, 1975.

LINK [18] W. W. Tait, “The completeness of Heyting first-order logic,” Journal of Symbolic Logic, vol. 68, no. 3, 751-763, 2003.

LINK [19] M. Tatsuta and G. Mints, “A Simple Proof of Second Order Strong Normalization with Permutative Conversions,” Annals of Pure and Applied Logic, 136(1-2) (2005)134-155.

LINK [20] A. S. Troelstra, “Metamathematical Investigation of Intuitionistic Arithmetic and Analysis,” Lecture Notes in Mathematics, vol. 344, 1973.

LINK [21] A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, 2nd. ed., 2000.