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

F. Barbanera, M. Dezani-ciancaglini, and U. De-'liguoro, Intersection and Union Types: Syntax and Semantics, Information and Computation, vol.119, issue.2, pp.202-230, 1995.
DOI : 10.1006/inco.1995.1086
URL : http://doi.org/10.1006/inco.1995.1086

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

F. Blanqui and C. Riba, Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems, LPAR'06, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00084837

T. Coquand and A. Spiwack, A Proof of Strong Normalisation using Domain Theory, LiCS'06, pp.307-316, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00432490

V. Danos and J. Krivine, Disjunctive Tautologies as Synchronisation Schemes, CSL'00, pp.292-301, 2000.
DOI : 10.1007/3-540-44622-2_19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2792

M. Dezani-ciancaglini, U. De-'liguoro, and P. Piperno, Filter models for conjunctive-disjunctive ??-calculi, Theoretical Computer Science, vol.170, issue.1-2, pp.83-128, 1996.
DOI : 10.1016/S0304-3975(96)80703-1
URL : http://doi.org/10.1016/s0304-3975(96)80703-1

M. Dezani-ciancaglini, U. De-'liguoro, and P. Piperno, A Filter Model for Concurrent $\lambda$-Calculus, SIAM Journal on Computing, vol.27, issue.5, pp.1376-1419, 1998.
DOI : 10.1137/S0097539794275860

M. Dezani-ciancaglini, J. Tiuryn, and P. Urzyczyn, Discrimination by parallel observers, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, 1997.
DOI : 10.1109/LICS.1997.614965
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.5112

A. Frisch, G. Castagna, and V. Benzaken, Semantic Subtyping, LICS'02, 2002.
DOI : 10.1109/lics.2002.1029823
URL : https://hal.archives-ouvertes.fr/hal-00152690

J. Gallier, Typing Untyped Lambda-Terms, or Reducibility Strikes Again! Annals of Pure and Applied Logic, pp.231-270, 1998.

H. Hosoya, J. Vouillon, and B. Pierce, Regular Expression Types for XML, ICFP'00, 2000.
DOI : 10.1145/357766.351242
URL : https://hal.archives-ouvertes.fr/hal-00009271

J. Krivine, Lambda-Calcul, Types et Modèles, p.12, 1990.
DOI : 10.1051/ita/1991250100671
URL : http://archive.numdam.org/article/ITA_1991__25_1_67_0.pdf

M. Parigot, Abstract, The Journal of Symbolic Logic, vol.50, issue.04, pp.1461-1479, 1997.
DOI : 10.1145/322358.322370

A. M. Pitts, Parametric polymorphism and operational equivalence, Mathematical Structures in Computer Science, vol.10, issue.3, pp.321-359, 2000.
DOI : 10.1017/S0960129500003066

C. Riba, On the Stability by Union of Reducibility Candidates, FoSSaCS'07, 2007.
DOI : 10.1007/978-3-540-71389-0_23
URL : https://hal.archives-ouvertes.fr/hal-00123116

F. Von-raamsdonk and P. Severi, On Normalisation, 1995.

J. Vouillon, Subtyping Union Types, CSL'04, pp.415-429, 2004.
DOI : 10.1007/978-3-540-30124-0_32
URL : https://hal.archives-ouvertes.fr/hal-00012706

J. Vouillon and P. Mellì-es, Semantic Types: A Fresh Look at the Ideal Model for Types, POPL'04, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00150968