A. Abel, Semi-continuous sized types and termination, Logical Methods in Computer Science, vol.4, issue.2, pp.1-33, 2008.

G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004.
DOI : 10.1017/S0960129503004122

F. Blanqui, Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations, Proc. of CSL'05
DOI : 10.1007/11538363_11
URL : https://hal.archives-ouvertes.fr/inria-00000200

F. Blanqui, Termination and Confluence of Higher-Order Rewrite Systems, Proc. of RTA'00
DOI : 10.1007/10721975_4
URL : https://hal.archives-ouvertes.fr/inria-00105556

F. Blanqui, A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems, Proc. of RTA'04
DOI : 10.1007/978-3-540-25979-4_2
URL : https://hal.archives-ouvertes.fr/inria-00100254

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-92, 2005.
DOI : 10.1017/S0960129504004426
URL : https://hal.archives-ouvertes.fr/inria-00105568

F. Blanqui and C. Riba, Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems, Proc. of LPAR'06
URL : https://hal.archives-ouvertes.fr/inria-00084837

F. Blanqui and C. Roux, On the relation between sized-types based termination and semantic labelling (full version). www-rocq.inria.fr, 2009.

H. Doornbos and B. Von-karger, On the union of well-founded relations, Logic Journal of IGPL, vol.6, issue.2, pp.195-201, 1998.
DOI : 10.1093/jigpal/6.2.195

M. Fiore, G. Plotkin, and D. Turi, Abstract syntax and variable binding, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)
DOI : 10.1109/LICS.1999.782615

E. Giménez, Un Calcul de Constructions infinies et son applicationàapplicationà la vérification de systèmes communiquants Interprétation fonctionelle etéliminationetélimination des coupures dans l'arithmetique d'ordre supérieur, 1972.

M. Hamana, Higher-order semantic labelling for inductive datatype systems, Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming, PPDP '07
DOI : 10.1145/1273920.1273933

M. Hamana, Universal Algebra for Termination of Higher-Order Rewriting, Proc. of RTA'05
DOI : 10.1007/978-3-540-32033-3_11

N. Hirokawa and A. Middeldorp, Predictive Labeling, Proc. of RTA'06
DOI : 10.1007/11805618_24

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96
DOI : 10.1145/237721.240882

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

N. P. Mendler, Inductive Definition in Type Theory, 1987.

A. Middeldorp, H. Ohsaki, and H. Zantema, Transforming termination by selflabelling, Proc. of CADE'96

D. Miller, A logic programming language with lambda-abstraction, function variables , and simple unification, Proc. of ELP'89

H. Xi, Dependent types for program termination verification, Proc. of LICS'01

H. Zantema, Termination of term rewriting by semantic labelling, Fundamenta Informaticae, vol.24, pp.89-105, 1995.