T. Aoto and T. Yamada, Termination of Simply Typed Term Rewriting by Translation and Labelling, Rewriting Techniques and Applications, 2003.
DOI : 10.1007/3-540-44881-0_27

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8
URL : http://doi.org/10.1016/s0304-3975(99)00207-8

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

C. Benzmüller and D. Miller, Automation of Higher-Order Logic, Computational Logic, Handbook of the History of Logic, pp.215-254, 2014.
DOI : 10.1016/B978-0-444-51624-4.50005-8

J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban, Hammering towards QED, J. Formalized Reasoning, vol.9, issue.1, pp.101-148, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01386988

J. C. Blanchette and T. Nipkow, Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, Interactive Theorem Proving, pp.131-146, 2010.
DOI : 10.1007/978-3-642-14052-5_11

J. C. Blanchette, U. Waldmann, and D. Wand, Formalization of recursive path orders for lambda-free higher-order terms. Archive of Formal Proofs (2016), formal proof development

J. C. Blanchette, U. Waldmann, and D. Wand, A Lambda-Free Higher-Order Recursive??Path??Order, 2016.
DOI : 10.1007/3-540-45127-7_25
URL : https://hal.archives-ouvertes.fr/hal-01592189

F. Blanqui, Termination and Confluence of Higher-Order Rewrite Systems, Rewriting Techniques and Applications (RTA 2000), pp.47-61, 2000.
DOI : 10.1007/10721975_4
URL : https://hal.archives-ouvertes.fr/inria-00105556

F. Blanqui, J. Jouannaud, and A. Rubio, The computability path ordering, Logical Methods in Computer Science, vol.11, issue.4, 2015.
DOI : 10.2168/LMCS-11(4:3)2015
URL : https://hal.archives-ouvertes.fr/hal-01163091

F. Blanqui and A. Koprowski, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Mathematical Structures in Computer Science, vol.37, issue.04, pp.827-859, 2011.
DOI : 10.1016/S0890-5401(03)00011-7
URL : https://hal.archives-ouvertes.fr/inria-00543157

M. Bofill, C. Borralleras, E. Rodríguez-carbonell, and A. Rubio, The recursive path and polynomial ordering for first-order and higher-order terms, Journal of Logic and Computation, vol.23, issue.1, pp.263-305, 2013.
DOI : 10.1093/logcom/exs027

M. Bofill and A. Rubio, Paramodulation with Non-Monotonic Orderings and Simplification, Journal of Automated Reasoning, vol.19, issue.4, pp.51-98, 2013.
DOI : 10.1007/978-3-642-76771-5

M. Codish, J. Giesl, P. Schneider-kamp, and R. Thiemann, SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs, Journal of Automated Reasoning, vol.56, issue.1, pp.53-93, 2012.
DOI : 10.1007/s10472-009-9144-7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.186.7933

É. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain, Automated certified proofs with CiME3, Rewriting Techniques and Applications (RTA '11)
URL : https://hal.archives-ouvertes.fr/hal-00777669

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://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.145.8728

H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli, DPLL(T): Fast Decision Procedures, Computer Aided Verification, pp.175-188, 2004.
DOI : 10.1007/978-3-540-27813-9_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.8015

L. Henkin, Completeness in the theory of types, The Journal of Symbolic Logic, vol.14, issue.02, pp.81-91, 1950.
DOI : 10.1007/BF01696781

N. Hirokawa, A. Middeldorp, and H. Zankl, Uncurrying for Termination and Complexity, Journal of Automated Reasoning, vol.50, issue.5, pp.279-315, 2013.
DOI : 10.1007/s00200-007-0046-9
URL : https://link.springer.com/content/pdf/10.1007%2Fs10817-012-9248-3.pdf

G. Huet and D. C. Oppen, Equations and rewrite rules: A survey Formal Language Theory: Perspectives and Open Problems, pp.349-405, 1980.
DOI : 10.1016/b978-0-12-115350-2.50017-8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.397.599

R. J. Hughes, Super-combinators a new implementation method for applicative languages, Proceedings of the 1982 ACM symposium on LISP and functional programming , LFP '82, pp.1-10, 1982.
DOI : 10.1145/800068.802129
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.472.4622

J. Jouannaud and A. Rubio, A recursive path ordering for higher-order terms in ?-long ?normal form, Rewriting Techniques and Applications (RTA-96)

J. Jouannaud and A. Rubio, Polymorphic higher-order recursive path orderings, Journal of the ACM, vol.54, issue.1, pp.1-248, 2007.
DOI : 10.1145/1206035.1206037
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.78.1121

R. Kennaway, J. W. Klop, M. R. Sleep, and F. De-vries, Comparing Curried and Uncurried Rewriting, Journal of Symbolic Computation, vol.21, issue.1, pp.15-39, 1996.
DOI : 10.1006/jsco.1996.0002

C. Kop, Higher Order Termination, 2012.

C. Kop and F. Van-raamsdonk, A Higher-Order Iterative Path Ordering, Logic for Programming, pp.697-711, 2008.
DOI : 10.1007/978-3-540-89439-1_48
URL : http://dare.ubvu.vu.nl/bitstream/1871/34190/1/219615.pdf

M. Lifantsev and L. Bachmair, An LPO-based termination ordering for higher-order terms without ??-abstraction, Theorem Proving in Higher Order Logics (TPHOLs '98), pp.277-293, 1998.
DOI : 10.1007/BFb0055142

O. Lysne and J. Piris, A termination ordering for higher order rewrite systems, ) Rewriting Techniques and Applications (RTA-95). LNCS, pp.26-40, 1995.
DOI : 10.1007/3-540-59200-8_45
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.9837

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, Handbook of Automated Reasoning, pp.371-443, 2001.
DOI : 10.1016/B978-044450813-3/50009-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.6344

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

C. Sternagel and R. Thiemann, Generalized and Formalized Uncurrying, Frontiers of Combining Systems, pp.243-258, 2011.
DOI : 10.1007/978-3-642-03359-9_31
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.231.9059

R. Thiemann, G. Allais, and J. Nagele, On the formalization of termination techniques based on multiset orderings, ) Rewriting Techniques and Applications (RTA '12). LIPIcs Schloss Dagstuhl?Leibniz-Zentrum für Informatik, pp.339-354, 2012.

R. Thiemann and C. Sternagel, Certification of Termination Proofs Using CeTA, Theorem Proving in Higher Order Logics, pp.452-468, 2009.
DOI : 10.1007/978-3-540-25979-4_6

Y. Toyama, Termination of S-Expression Rewriting Systems: Lexicographic Path Ordering for Higher-Order Terms, Rewriting Techniques and Applications (RTA 2004). LNCS, pp.40-54, 2004.
DOI : 10.1007/978-3-540-25979-4_3

D. A. Turner, A new implementation technique for applicative languages, Software: Practice and Experience, vol.6, issue.1, pp.31-49, 1979.
DOI : 10.1093/comjnl/6.4.308

T. Yamada, Confluence and Termination of Simply Typed Term Rewriting Systems, ) Rewriting Techniques and Applications (RTA 2001), pp.338-352, 2001.
DOI : 10.1007/3-540-45127-7_25