A. Abel, Termination checking with types, Theoretical informatics and applications, pp.277-319, 2004.
DOI : 10.1093/comjnl/45.4.436

A. Abel, A polymorphic lambda-calculus with sized higher-order types, 2006.

A. Abel, Semi-continuous sized types and termination, Logical methods in computer science, vol.4, issue.2, pp.1-33, 2008.
DOI : 10.1007/11874683_5

A. Abel, MiniAgda: Integrating Sized and Dependent Types, Proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers, Electronic Proceedings in Theoretical Computer Science 43, 2010.
DOI : 10.1007/3-540-58085-9_72

A. Abel, Type-Based Termination, Inflationary Fixed-Points, and Mixed Inductive-Coinductive Types, Proceedings of the 8th Workshop on Fixed-points in Computer Science, Electronic Proceedings in Theoretical Computer Science 77, 2012.
DOI : 10.1023/A:1019916231463
URL : http://www.tcs.ifi.lmu.de/%7Eabel/fics12.pdf

A. Abel and T. Altenkirch, A predicative analysis of structural recursion, Journal of Functional Programming, vol.12, issue.01, pp.1-41, 2002.
DOI : 10.1017/S0956796801004191

W. Ackermann, Begr???ndung des ?tertium non datur? mittels der Hilbertschen Theorie der Widerspruchsfreiheit, Mathematische Annalen, vol.93, issue.1, pp.1-36, 1925.
DOI : 10.1007/BF01449946

. Agda, Agda, a dependently typed functional programming language and proof assistant, 2016.

R. Amadio and S. Coupet-grimal, Analysis of a guard condition in type theory (preliminary report), 1997.
URL : https://hal.archives-ouvertes.fr/inria-00073388

R. Amadio and S. Coupet-grimal, Analysis of a guard condition in type theory (Extended abstract), Proceedings of the 1st International Conference on Foundations of Software Science and Computation Structures, 1378.

T. Arts, Termination by absence of infinite chains of dependency pairs, Proceedings of the 21st Colloquium on Trees in Algebra and Programming, 1059.
DOI : 10.1007/3-540-61064-2_38

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs. Theoretical computer science, pp.133-178, 2000.

M. Avanzini and G. Moser, Closing the gap between runtime complexity and polytime computability, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics 6, 2010.

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization in the algebraic-??-cube, Journal of Functional Programming, vol.7, issue.6, pp.613-660, 1997.
DOI : 10.1017/S095679689700289X

G. Barthe, B. Grégoire, and F. Pastawski, Practical Inference for Type-Based Termination in a Polymorphic Setting, Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, 2005.
DOI : 10.1007/11417170_7

G. Barthe, B. Grégoire, and F. Pastawski, CIC: Type-Based Termination of Recursive Definitions in the Calculus, of Induc Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2006.

A. M. Ben-amram and M. Codish, A SAT-Based Approach to Size Change Termination with Global Ranking Functions, Proceedings of the 14th International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 2008.
DOI : 10.1007/978-3-540-78800-3_16

U. Berger, Continuous Semantics for Strong Normalization, Proceedings of the 1st Conference on Computability in Europe, 2005.
DOI : 10.1007/11494645_4

U. Berger, A domain model characterising strong normalisation. Annals of pure and applied logic, pp.39-50, 2008.

F. Blanqui, Termination and Confluence of Higher-Order Rewrite Systems, Proceedings of the 11th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 1833, 2000.
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, Proceedings of the 15th International Conference on Rewriting Techniques and Applications, 2004.
DOI : 10.1007/978-3-540-25979-4_2
URL : https://hal.archives-ouvertes.fr/inria-00100254

F. Blanqui, Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations, Proceedings of the 19th International Conference on Computer Science Logic, 2005.
DOI : 10.1007/11538363_11
URL : https://hal.archives-ouvertes.fr/inria-00000200

F. Blanqui, Definitions by rewriting in the calculus of constructions, Mathematical structures in computer science, pp.37-92, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00105648

F. Blanqui, Higher-order dependency pairs, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00084821

F. Blanqui, (HO)RPO revisited, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00090488

F. Blanqui, HOT, an automated termination prover for higher-order rewrite systems, 2012.

F. Blanqui, Termination of rewrite relations on ? -terms based on Girard's notion of reducibility. Theoretical computer science, pp.50-86, 2016.

F. Blanqui and C. Riba, Combining typing and size constraints for checking the termination of higher-order conditional rewrite, Proceedings of the 13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00084837

F. Blanqui and C. Roux, On the Relation between Sized-Types Based Termination and Semantic Labelling, Proceedings of the 23rd International Conference on Computer Science Logic, 2009.
DOI : 10.1007/BFb0038698
URL : https://hal.archives-ouvertes.fr/inria-00397689

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, J. Jouannaud, and A. Rubio, The computability path ordering, Logical Methods in Computer Science, vol.11, issue.4, pp.1-45, 2015.
DOI : 10.2168/LMCS-11(4:3)2015
URL : https://hal.archives-ouvertes.fr/hal-01163091

G. Bonfante, J. Marion, and R. Péchoux, Quasi-interpretations a way to control resources. Theoretical computer science, pp.2776-2796, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00591862

C. Borralleras and A. Rubio, A Monotonic Higher-Order Semantic Path Ordering, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2001.
DOI : 10.1007/3-540-45653-8_37

C. Borralleras and A. Rubio, THOR, a tool for proving the termination of higher-order rewrite systems, 2014.

R. Boyer and J. Moore, A computational logic, 1979.

V. Breazu-tannen and J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Proceedings of the 16th International Colloquium on Automata, Languages and Programming, 1989.
DOI : 10.1016/0304-3975(91)90037-3
URL : https://doi.org/10.1016/0304-3975(91)90037-3

R. Burstall, D. Queen, . Mac, and D. Sannella, HOPE, Proceedings of the 1980 ACM conference on LISP and functional programming , LFP '80, 1980.
DOI : 10.1145/800087.802799

J. Cheney, First-class phantom types, 2003.

A. Cherifa, . Ben, and P. Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation, Science of Computer Programming, vol.9, issue.2, pp.137-159, 1987.
DOI : 10.1016/0167-6423(87)90030-X
URL : https://hal.archives-ouvertes.fr/inria-00075876

W. N. Chin and S. C. Khoo, Calculating sized types Journal of higher-order and symbolic computation, pp.261-300, 2001.

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

E. A. Cicho´ncicho´n and H. Touzet, An ordinal calculus for proving termination in term rewriting, Proceedings of the 21st Colloquium on Trees in Algebra and Programming, 1059.

M. Clavel, F. Durán, S. Eker, S. Escobar, P. Lincoln et al., Maude 2.7 manual, 2011.

G. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decompostion, Proceedings of the 2nd GI conference on Automata Theory and Formal Languages, 1975.
DOI : 10.1007/3-540-07407-4_17

. Coq, The Coq reference manual, version 8.6, 2016.

T. Coquand and C. Paulin-mohring, Inductively defined types, Proceedings of the International Conference on Computer Logic, 1988.
DOI : 10.1007/3-540-52335-9_47

T. Coquand and A. Spiwack, A proof of strong normalization using domain theory, Logical methods in computer science, vol.3, issue.4, pp.1-16, 2007.

P. Courtieu, G. Gbedo, and O. Pons, Improved Matrix Interpretation, Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science, 2010.
DOI : 10.1007/978-3-642-11266-9_24
URL : https://hal.archives-ouvertes.fr/hal-01125706

P. Cousot, Abstract interpretation, ACM Computing Surveys, vol.28, issue.2, pp.324-328, 1996.
DOI : 10.1145/234528.234740
URL : https://hal.archives-ouvertes.fr/hal-00930103

P. Cousot, Types as abstract interpretations, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '97, 1997.
DOI : 10.1145/263699.263744

P. Cousot and R. Cousot, Constructive versions of Tarski???s fixed point theorems, Pacific Journal of Mathematics, vol.82, issue.1, pp.43-57, 1979.
DOI : 10.2140/pjm.1979.82.43

R. Cuninghame-green, Minimax algebra, Lecture Notes in Economics and Mathematical Systems, vol.166, issue.166, 1979.
DOI : 10.1007/978-3-642-48708-8

P. Curien and G. Ghelli, Coherence of subsumption, minimum typing and type-checking in F ???, Logical methods in computer science, pp.55-91, 1992.
DOI : 10.1016/0890-5401(90)90062-M

H. B. Curry and R. Feys, Combinatory logic, 1958.

N. G. De-bruijn, The mathematical language AUTOMATH, its usage, and some of its extensions, Proceedings of the 1968 Symposium on Automatic Demonstration, 1970.

R. De-vrijer, Exactly estimating functionals and strong normalization, Indagationes Mathematicae (Proceedings), vol.90, issue.4, pp.479-493, 1987.
DOI : 10.1016/1385-7258(87)90012-6

N. Dershowitz, A note on simplification orderings, Information Processing Letters, vol.9, issue.5, pp.212-215, 1979.
DOI : 10.1016/0020-0190(79)90071-1

N. Dershowitz, Orderings for term rewriting systems, Proceedings of the 20th IEEE Symposium on Foundations of Computer Science, 1979.

N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982.
DOI : 10.1016/0304-3975(82)90026-3

N. Dershowitz, Dependency Pairs are a Simple Semantic Path Ordering, 2013.

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science. Volume B: formal models and methods, pp.243-320, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

N. Dershowitz and Z. Manna, Proving termination with multiset orderings, Communications of the ACM, vol.22, issue.8, pp.465-476, 1979.
DOI : 10.1145/359138.359142
URL : http://www.dtic.mil/get-tr-doc/pdf?AD%3DADA058601%26Location%3DU2%26doc%3DGetTRDoc.pdf

N. Dershowitz and M. Okada, Proof-theoretic techniques for term rewriting theory, [1988] Proceedings. Third Annual Information Symposium on Logic in Computer Science, 1988.
DOI : 10.1109/LICS.1988.5108

J. Endrullis, J. Waldmann, and H. Zantema, Matrix Interpretations for Proving Termination of Term Rewriting, Journal of Automated Reasoning, vol.17, issue.4, pp.195-220, 2008.
DOI : 10.1007/s10817-007-9087-9

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

Y. Fuh and P. Mishra, Type inference with subtypes. Theoretical computer science, pp.155-175, 1990.
DOI : 10.1016/0304-3975(90)90144-7
URL : https://doi.org/10.1016/0304-3975(90)90144-7

C. Fuhs and C. Kop, Polynomial interpretations for higher-order rewriting, Proceedings of the 23rd International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics 15, 2012.

C. Fuhs, J. Giesl, A. Middeldorp, P. Schneider-kamp, R. Thiemann et al., SAT Solving for Termination Analysis with Polynomial Interpretations, Proceedings of the 10th ZU064-05-FPR main 12, p.15, 2007.
DOI : 10.1007/978-3-540-72788-0_33

C. Fuhs, R. Navarro, C. Otto, J. Giesl, S. Lucas et al., Search Techniques for Rational Polynomial Orders, Proceedings of the 9th International Conference on Artificial Intelligence and Symbolic Computation, 2008.
DOI : 10.1007/978-3-540-85110-3_10

R. O. Gandy, An early proof of normalization by A. M. Turing. Pages 453?455 of, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.

R. O. Gandy, Proofs of strong normalization. Pages 457?477 of, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 1980.

G. Gentzen, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische Annalen, vol.25, issue.1, pp.493-565, 1935.
DOI : 10.1007/BF01565428

J. Giesl, Termination of nested and mutually recursive algorithms, Journal of Automated Reasoning, vol.19, issue.1, pp.1-29, 1997.
DOI : 10.1023/A:1005797629953

J. Giesl, T. Arts, and E. Ohlebusch, Modular Termination Proofs for Rewriting Using Dependency Pairs, Journal of Symbolic Computation, vol.34, issue.1, pp.21-58, 2002.
DOI : 10.1006/jsco.2002.0541

E. Giménez, Un calcul de constructions infinies et son application à la vérification de systèmes communiquants, 1996.

E. Giménez, Structural recursive definitions in type theory, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, 1443.
DOI : 10.1007/BFb0055070

J. Girard, Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur, 1972.

J. Girard, Y. Lafont, and P. Taylor, Proofs and types, 1988.

K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für mathematik und physik, pp.173-198, 1931.

K. Gödel, Collected works, pp.1938-1974, 1990.

B. Grégoire and J. L. Sacchini, On Strong Normalization of the Calculus of Constructions with Type-Based Termination, Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2010.
DOI : 10.1007/BFb0097796

M. Hamana, An initial algebra approach to term rewriting systems with variable binders Journal of higher-order and symbolic computation, pp.231-262, 2006.

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, 2007.
DOI : 10.1145/1273920.1273933

G. H. Hardy, A theorem concerning the infinite cardinal numbers, Quarterly journal of mathematics, vol.35, pp.87-94, 1904.

F. Hartogs, ???ber das Problem der Wohlordnung, Mathematische Annalen, vol.76, issue.4, pp.438-443, 1915.
DOI : 10.1007/BF01458215

J. Herbrand, Recherches sur la théorie de la démonstration, Faculté des sciences de, 1930.

G. Hessenberg, Kettentheorie und Wohlordnung, Journal für die reine und angewandte Mathematik, pp.81-133, 1909.

R. Hindley, The Principal Type-Scheme of an Object in Combinatory Logic, Transactions of the American Mathematical Society, vol.146, pp.29-60, 1969.
DOI : 10.2307/1995158

N. Hirokawa and A. Middeldorp, Automating the dependency pair method. Information and computation, pp.172-199, 2005.

N. Hirokawa and A. Middeldorp, Predictive Labeling, Proceedings of the 17th International Conference on Rewriting Techniques and Applications, 2006.
DOI : 10.1007/11805618_24

D. Hofbauer and C. Lautemann, Termination proofs and the length of derivations, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, 1989.
DOI : 10.1007/3-540-51081-8_107

M. Hofmann, Approaches to recursive data types -a case study, p.61, 1995.

H. Hong and D. Jaku?, Testing positiveness of polynomials, Journal of Automated Reasoning, vol.21, issue.1, pp.23-38, 1998.
DOI : 10.1023/A:1005983105493

W. A. Howard, Assignment of Ordinals to Terms for Primitive Recursive Functionals of Finite Type, Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N. Y. Studies in Logic and the Foundations of Mathematics, 1970.
DOI : 10.1016/S0049-237X(08)70770-5

W. A. Howard, A system of abstract constructive ordinals, The Journal of Symbolic Logic, vol.20, issue.02, pp.355-374, 1972.
DOI : 10.1111/j.1746-8361.1958.tb01464.x

K. Hrbacek and T. Jech, Introduction to set theory, 1999.

G. Huet, Résolution d'équations dans les langages d'ordre 1, Thèse d'État, 1976.

G. Huet and J. Hullot, Proofs by induction in equational theories with constructors, Journal of Computer and System Sciences, vol.25, issue.2, pp.239-266, 1982.
DOI : 10.1016/0022-0000(82)90006-X
URL : https://hal.archives-ouvertes.fr/inria-00076533

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, 1996.
DOI : 10.1145/237721.240882

P. Hyvernat, The Size-Change Termination Principle for Constructor Based Languages, Logical methods in computer science, vol.10, issue.1, pp.1-30, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00547440

N. D. Jones and N. Bohr, Call-by-value Termination in the Untyped ??-calculus, Logical methods in computer science, pp.1-39, 2008.
DOI : 10.2168/LMCS-4(1:3)2008

J. Jouannaud and M. Okada, A computation model for executable higher-order algebraic specification languages, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, 1991.
DOI : 10.1109/LICS.1991.151659

J. Jouannaud and A. Rubio, The higher-order recursive path ordering, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999.
DOI : 10.1109/LICS.1999.782635

J. Jouannaud and A. Rubio, Polymorphic higher-order recursive path orderings, Journal of the ACM, vol.54, issue.1, pp.1-48, 2007.
DOI : 10.1145/1206035.1206037
URL : http://www.lsi.upc.es/~albert/papers/jouannaudrubioJACM.pdf

S. Kahrs, Towards a domain theory for termination proofs, Proceedings of the 6th International Conference on Rewriting Techniques and Applications, 1995.
DOI : 10.1007/3-540-59200-8_60

S. Kamin and J. Lévy, Attempts for generalizing the recursive path orderings. Unpublished note, 1980.

B. Knaster and A. Tarski, Un théorème sur les fonctions d'ensembles. Annales de la société polonaise de mathématiques, pp.133-134, 1928.

C. Kop, Higher order dependency pairs for algebraic functional systems, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, Leibniz International Proceedings in Informatics 10, 2011.
DOI : 10.2168/lmcs-8(2:10)2012
URL : https://lmcs.episciences.org/668/pdf

C. Kop, WANDA, a higher-order termination tool, 2015.

A. Koprowski and H. Zantema, Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems, Proceedings of the 3rd International Joint Conference on Automated Reasoning, 2006.
DOI : 10.1007/11814771_30

C. Kuratowski, Une méthode d'élimination des nombres transfinis des raisonnements mathématiques. Fundamenta mathematicae, pp.76-108, 1922.
DOI : 10.4064/fm-3-1-76-108

K. Kusakari and M. Sakai, Enhancing dependency pair method using strong computability in simply-typed term rewriting syst Applicable algebra in engineering communication and computing, pp.407-431, 2007.

S. Lucas, Polynomials over the reals in proofs of termination : from theory to practice, Theoretical informatics and applications, pp.547-586, 2005.
DOI : 10.1007/3-540-62950-5_69

Z. Manna and S. Ness, On the termination of Markov algorithms, Proceedings of the 3rd Hawaii International Conference on System Sciences, 1970.

Y. V. Matiyasevich, Enumerable sets are diophantine, pp.354-358, 1970.

Y. V. Matiyasevich, Hilbert's tenth problem, 1993.

R. Matthes, Lambda calculus: a case for inductive definitions, 2000.

R. Mayr and T. Nipkow, Higher-order rewrite systems and their confluence. Theoretical computer science, pp.3-29, 1998.
DOI : 10.1016/s0304-3975(97)00143-6

N. P. Mendler, Inductive definition in type theory, 1987.

N. P. Mendler, Inductive types and type constraints in the second-order lambda calculus. Annals of pure and applied logic, pp.159-172, 1991.

A. Middeldorp, H. Ohsaki, and H. Zantema, Transforming termination by self-labelling, Proceedings of the 13th International Conference on Automated Deduction, 1104.
DOI : 10.1007/3-540-61511-3_101

D. Miller, A logic programming language with lambda-abstraction, function variables, and simple unification, Proceedings of the International Workshop on Extensions of Logic Programming, 1991.

R. Milner, A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol.17, issue.3, pp.348-375, 1978.
DOI : 10.1016/0022-0000(78)90014-4

. Miniagda, MiniAgda, 2014.

J. Mitchell, Coercion and type inference (summary), Proceedings of the 11th ACM Symposium on Principles of Programming Languages, 1984.
DOI : 10.1145/800017.800529

F. Monin and M. Simonot, An ordinal measure based procedure for termination of functions. Theoretical computer science, pp.63-94, 2001.

G. Moser, KBOs, ordinals, subrecursive hierarchies and all that, Journal of Logic and Computation, vol.27, issue.2, pp.1-27, 2014.
DOI : 10.1093/logcom/exu072

M. Newman, On Theories with a Combinatorial Definition of "Equivalence", The Annals of Mathematics, vol.43, issue.2, pp.223-243, 1942.
DOI : 10.2307/1968867

T. Nipkow, Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, 1991.
DOI : 10.1109/LICS.1991.151658

M. Okada, Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term, Proceedings of the International Symposium on Symbolic and Algebraic Computation, 1989.

L. Pareto, Types for crash prevention, 2000.

L. Paulson, Proving termination of normalization functions for conditional expressions, Journal of Automated Reasoning, vol.2, issue.1, pp.63-74, 1986.
DOI : 10.1007/BF00246023

G. Peano, Arithmetices principia, nova methodo exposita. Fratres Bocca, 1889.

S. Peyton-jones, Haskell 98 language and libraries, the revised report, 2003.

G. D. 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

F. Pottier, Simplifying subtyping constraints: a theory. Information and computation, pp.153-183, 2001.

V. Pratt, Two easy theories whose combination is hard, 1977.

M. Presburger, Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, welchem die Addition als einzige Operation hervortritt. Sprawozdanie z I Kongresu Matematykow Krajow Slowcanskich, 1929.

M. Rathjen, The art of ordinal analysis, Pages 45?69 of: Proceedings of the International Congress of Mathematicians, 2006.
DOI : 10.4171/022-2/3

C. Riba, On the Stability by Union of Reducibility Candidates, Proceedings of the 10th International Conference on Foundations of Software Science and Computation Structures, 2007.
DOI : 10.1007/978-3-540-71389-0_23
URL : https://hal.archives-ouvertes.fr/hal-00123116

C. Riba, Stability by union of reducibility candidates for orthogonal constructor rewriting, Proceedings of the 4th Conference on Computability in Europe, 2008.

C. Riba, On the Values of Reducibility Candidates, Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications, 2009.
DOI : 10.1007/978-3-540-73228-0_26
URL : https://hal.archives-ouvertes.fr/hal-00800668

J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

H. Rubin and J. E. Rubin, Equivalents of the axiom of choice, 1963.

J. L. Sacchini, On Type-Based Termination and Dependent Pattern Matching in the Calculus of Inductive Constructions, 2011.
URL : https://hal.archives-ouvertes.fr/pastel-00622429

J. L. Sacchini, Cicminus, Coq with type-based termination, 2015.

M. Sakai, Y. Watanabe, and T. Sakabe, An extension of dependency pair method for proving termination of higher-order rewrite systems, Ieice transactions on information and systems, issue.8, pp.84-1025, 2001.

S. Schmitz, Complexity Bounds for Ordinal-Based Termination (invited talk) Pages 1?19 of: Proceedings of the 8th International Workshop on Reachability Problems, Lecture Notes in Computer Science, vol.8762, 2014.

D. S. Scott, Continuous lattices. Pages 97?136 of Toposes, algebraic geometry and logic, Lecture Notes in Mathematics, issue.274, 1972.

M. P. Sellink, Verifying Process Algebra Proofs in Type Theory, Proceedings of the 1st International Workshop on Semantics of Specification Languages, 1993.
DOI : 10.1007/978-1-4471-3229-5_18

C. Sprenger and M. Dam, On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the ??Calculus, Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures, 2003.
DOI : 10.1007/3-540-36576-1_27

C. Sternagel and A. Middeldorp, Root-Labeling, Proceedings of the 19th International Conference on Rewriting Techniques and Applications, 2008.
DOI : 10.1007/978-3-540-70590-1_23

C. Sternagel and R. Thiemann, Signature extensions preserve termination -an alternative proof via dependency pairs, Proceedings of the 24th International Conference on Computer Science Logic, 2010.

M. Sulzmann, A general framework for Hindley/Milner type systems with constraints, 2000.

M. Sulzmann, A General Type Inference Framework for Hindley/Milner Style Systems, Proceedings of the 5th Fuji International Symposium on Functional and Logic Programming, 2001.
DOI : 10.1007/3-540-44716-4_16

M. E. Szabo, Collected papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics, 1969.

W. W. Tait, Intensional interpretations of functionals of finite type I, The Journal of Symbolic Logic, vol.91, issue.02, pp.198-212, 1967.
DOI : 10.1007/BF01447860

A. Tarski, A Decision Method for Elementary Algebra and Geometry, 1948.
DOI : 10.1007/978-3-7091-9459-1_3

A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics, vol.5, issue.2, pp.285-309, 1955.
DOI : 10.2140/pjm.1955.5.285

A. Telford and D. Turner, Ensuring termination in ESFP, Proceedings of the 15th British Colloquium for Theoretical Computer Science, 2000.

R. Thiemann and J. Giesl, The size-change principle and dependency pairs for termination of term rewriting. Applicable algebra in engineering communication and computing, pp.229-270, 2005.

A. M. Turing, Some theorems about Church's system. Unpublished typescript reproduced in (Gandy, 1942.

J. Heijenoort, From Frege to Gödel, a source book in mathematical logic, pp.1879-1931, 1977.

J. Van-de-pol, Termination proofs for higher-order rewrite systems, Proceedings of the 1st International Workshop on Higher-Order Algebra, Logic and Term Rewriting, 1993.

J. J. Van-de-pol, Two different strong normalization proofs? Computability versus functionals of finite type Proceedings of the 2nd International Workshop on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science 1074 Termination of higher-order rewrite systems, 1995.

V. Van-oostrom, Confluence for abstract and higher-order rewriting, 1994.

D. Wahlstedt, Dependent type theory with first-order parameterized data types and well-founded recursion, 2007.

A. Weiermann, Abstract, The Journal of Symbolic Logic, vol.6, issue.04, pp.1348-1370, 1998.
DOI : 10.2307/421108

B. Werner, Une théorie des constructions inductives, 1994.

G. Wilken and A. Weiermann, Derivation Lengths Classification of Gödel's T Extending Howard's Assignment, Logical methods in computer science, vol.8, issue.1, pp.1-44, 2012.

H. Xi, Dependent types for program termination verification Journal of higher-order and symbolic computation, pp.91-131, 2002.

H. Xi, Applied Type System (extended abstract), Proceedings of the International Workshop on Types for Proofs and Programs, 2003.

H. Xi, C. Chen, and G. Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM Symposium on Principles of Programming Languages, 2003.
DOI : 10.1145/604131.604150
URL : http://www.church-project.org/reports/electronic/./Xi+Chen+Chen:POPL-2003.pdf.gz

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

C. Zenger, Indexed types. Theoretical computer science, pp.147-165, 1997.
DOI : 10.1016/s0304-3975(97)00062-5
URL : https://doi.org/10.1016/s0304-3975(97)00062-5