A. Abel, Termination Checking with Types Special Issue (FICS'03), RAIRO ? Theoretical Informatics and Applications, pp.277-319, 2004.

A. Abel, Semi-Continuous Sized Types and Termination, Proceedings of CSL'06, pp.72-88, 2006.
DOI : 10.2168/lmcs-4(2:3)2008
URL : http://arxiv.org/abs/0804.0876

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

H. P. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, 1992.
DOI : 10.1017/cbo9781139032636

G. Barthe, B. Grégoire, and F. Pastawski, CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions, Proceedings of LPAR'06, pp.257-271, 2006.
DOI : 10.1007/11916277_18

F. Blanqui, J. Jouannaud, and M. Okada, Inductive-data-type systems, Theoretical Computer Science, vol.272, issue.1-2, pp.41-68, 2002.
DOI : 10.1016/S0304-3975(00)00347-9
URL : https://hal.archives-ouvertes.fr/inria-00105578

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

V. Danos and J. Krivine, Disjunctive Tautologies as Synchronisation Schemes, Proceedings of 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

J. H. Gallier, On Girard's " Candidats de Reducibilité, Logic and Computer Science, 1989.

J. Girard, Interprétation Fonctionnelle etÉliminationet´etÉlimination des Coupures de l'Arithmétique d'Ordre Supérieur, 1972.

J. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4
URL : https://hal.archives-ouvertes.fr/inria-00075966

J. Glauert, D. Kesner, and Z. Khasidashvili, Expression Reduction Systems and Extensions: An Overview, Processes, Terms and Cycles: Steps to the Road of Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, pp.496-553, 2005.
DOI : 10.1007/11601548_22
URL : https://hal.archives-ouvertes.fr/hal-00148530

Z. Khasidashvili, M. Ogawa, and V. Van-oostrom, Perpetuality ans Uniform Normalization in Orthogonal Rewrite Systems. Information and Computation, pp.118-152, 2001.

J. Krivine, Lambda-Calcul, Types et Modèles, 1990.

N. P. Mendler, Recursive Types and Type Constraints in Second Order Lambda- Calculus, Proceedings of LiCS'87, pp.30-36, 1987.

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

C. Riba, Definitions par Réécriture dans le ?-Calcul: Confluence, Réductibilité et Typage, 2007.

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

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

W. W. Tait, A realizability interpretation of the theory of species, Logic Colloquium, pp.240-251, 1975.
DOI : 10.1007/BFb0064875

M. Tatsuta, Simple Saturated Sets for Disjunction and Second-Order Existential Quantification, Proceedings of TLCA'07, pp.366-380, 2007.
DOI : 10.1007/978-3-540-73228-0_26