A. Abel, Syntactical Normalization for Intersection Types with Term Rewriting Rules, 4th International Workshop on Higher-Order Rewriting, HOR'07, 2007.

P. Aczel, Frege Structures and the Notions of Proposition, Truth and Set, Stud. Logic Foundations Math, vol.101, pp.31-59, 1980.
DOI : 10.1016/S0049-237X(08)71252-7

. Th and . Altenkirch, Constructions, Inductive Types and Strong Normalization, 1993.

R. Amadio and P. L. Curien, Domains and Lambda-Calculi. Cambridge tracts in theoretical computer science, p.46, 1997.
URL : https://hal.archives-ouvertes.fr/inria-00070008

S. Van-bakel, Complete restrictions of the intersection type discipline, Theoretical Computer Science, vol.102, issue.1, pp.135-163, 1992.
DOI : 10.1016/0304-3975(92)90297-S

H. Barendregt, M. Coppo, and M. Dezani-ciancaglini, A filter lambda model and the completeness of type assignment, The Journal of Symbolic Logic, vol.37, issue.04, pp.931-940, 1983.
DOI : 10.1002/malq.19800261902

M. Beeson, Foundations of constructive mathematics. Metamathematical studies, Ergebnisse der Mathematik und ihrer Grenzgebiete (3) [Results in Mathematics and Related Areas, 1985.

S. Berardi, M. Bezem, . Th, and . Coquand, Abstract, The Journal of Symbolic Logic, vol.39, issue.02, pp.600-622, 1998.
DOI : 10.1007/BF02007566

U. Berger and P. Oliva, Modified Bar Recursion and Classical Dependent Choice. Logic Colloquium '01, Lect. Notes Log. Assoc. Symbol. Logic, vol.20, pp.89-107, 2005.

U. Berger, Continuous semantics for strong normalisation, Mathematical Structures in Computer Science, vol.16, issue.05, pp.23-34, 2005.
DOI : 10.1017/S0960129506005457

U. Berger, Strong normalization for applied lambda calculi, Logical Methods in Computer Science, vol.1, issue.2, pp.1-14, 2005.
DOI : 10.2168/LMCS-1(2:3)2005
URL : http://dx.doi.org/10.2168/lmcs-1(2:3)2005

U. Berger, Continuous Functionals of Dependent and Transfinite Types, Models and Computability, pp.1-22, 1999.
DOI : 10.1017/CBO9780511565670.002

J. W. Klop, V. Van-oostrom, and F. Van-raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, vol.121, issue.1-2, pp.279-308, 1993.
DOI : 10.1016/0304-3975(93)90091-7

P. Martin-löf, Lecture note on the domain interpretation of type theory, Workshop on Semantics of Programming Languages, 1983.

P. Martin-löf, An intuitionistic theory of types. in Twenty-five years of constructive type theory, pp.127-172, 1995.

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.

G. Plotkin, LCF considered as a programming language, Theoretical Computer Science, vol.5, issue.3, pp.223-255, 1977.
DOI : 10.1016/0304-3975(77)90044-5

C. Riba, Strong Normalization as Safe Interaction, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007.
DOI : 10.1109/LICS.2007.46
URL : https://hal.archives-ouvertes.fr/inria-00130456

D. Scott, Lectures on a mathematical theory of computation. Theoretical foundations of programming methodology, NATO Adv. Study Inst. Ser. C: Math. Phys. Sci, vol.91, pp.145-292, 1981.

D. Scott, Combinators and classes, Lecture Notes in Comput. Sci, vol.37, pp.1-26, 1975.
DOI : 10.1007/BFb0029517

C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, 1962.
DOI : 10.1090/pspum/005/0154801

. Th and . Streicher, Semantics of Type Theory. in the series Progress in Theoretical Computer Science, Basel: Birkhaeuser. XII, 1991.

W. W. Tait, Normal Form Theorem for Bar Recursive Functions of Finite Type, Proceedings of the Second Scandinavian Logic Symposium, 1971.
DOI : 10.1016/S0049-237X(08)70853-X