L. Bachmair and H. Ganzinger, Resolution Theorem Proving, Handbook of Automated Reasoning, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

J. Banâtre, P. Fradet, and Y. Radenac, Generalised multisets for chemical programming, Mathematical Structures in Computer Science, vol.16, issue.04, pp.557-580, 2006.
DOI : 10.1017/S0960129506005317

G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Journal of Functional Programming, vol.13, issue.02, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-01124972

H. Becker, J. C. Blanchette, U. Waldmann, and D. Wand, Formalization of Knuth?Bendix orders for lambda-free higher-order terms. Archive of Formal Proofs URL: https, 2016.

H. Becker, J. C. Blanchette, U. Waldmann, and D. Wand, A Transfinite Knuth???Bendix Order for Lambda-Free Higher-Order Terms, LNCS, vol.69, issue.1, p.26, 2017.
DOI : 10.1016/j.jsc.2014.09.033
URL : https://hal.archives-ouvertes.fr/hal-01592186

C. Blanchette, M. Fleury, and D. Traytel, Formalization of nested multisets, hereditary multisets, and syntactic ordinals. Archive of Formal Proofs URL: https, 2016.

J. Christian-blanchette, M. Fleury, and C. Weidenbach, A verified SAT solver framework with learn, forget, restart, and incrementality, IJCAR 2016, pp.25-44, 2016.

J. Christian-blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu et al., Truly modular (co)datatypes for Isabelle/HOL, ITP 2014, pp.93-110, 2014.

J. Christian-blanchette, A. Popescu, and D. Traytel, 10 Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand. A lambda-free higherorder recursive path order, ITP 2014 FoSSaCS 2017, pp.111-127, 2014.

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

L. Bulwahn, A. Krauss, and T. Nipkow, Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL, LNCS, vol.4732, pp.38-53, 2007.
DOI : 10.1007/978-3-540-74591-4_5

P. Castéran and É. Contejean, On ordinal notations Coq User Contributions, 2006.

E. Contejean, P. Courtieu, J. Forest, O. Pons, and X. Urbain, Certification of Automated Termination Proofs, LNCS, vol.4720, pp.148-162, 2007.
DOI : 10.1007/978-3-540-74621-8_10
URL : https://hal.archives-ouvertes.fr/hal-01125298

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

N. Dershowitz and G. Moser, The Hydra Battle Revisited, Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, pp.1-27, 2007.
DOI : 10.1007/978-3-540-73147-4_1

L. Goodstein, On the restricted ordinal theorem, The Journal of Symbolic Logic, vol.38, issue.02, pp.33-41, 1944.
DOI : 10.1007/BF01565428

. Grimm, Implementation of three types of ordinals in Coq
URL : https://hal.archives-ouvertes.fr/hal-00911710

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

B. Huffman and O. Kun?ar, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, CPP 2013, pp.131-146, 2013.
DOI : 10.1007/978-3-319-03545-1_9

C. Kaliszyk and C. Urban, Quotients revisited for Isabelle/HOL, Proceedings of the 2011 ACM Symposium on Applied Computing, SAC '11, pp.1639-1644, 2011.
DOI : 10.1145/1982185.1982529
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.3031

L. Kirby and J. Paris, Accessible Independence Results for Peano Arithmetic, Bulletin of the London Mathematical Society, vol.14, issue.4, pp.285-293, 1982.
DOI : 10.1112/blms/14.4.285
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.3303

A. Krauss, Partial Recursive Functions in Higher-Order Logic, LNCS, vol.4130, pp.589-603, 2006.
DOI : 10.1007/11814771_48

A. Krauss, Certified Size-Change Termination, LNCS, vol.4603, pp.21-460, 2007.
DOI : 10.1007/978-3-540-73595-3_34
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.91.8426

R. Loader, Unary PCF is decidable, Theoretical Computer Science, vol.206, issue.1-2, pp.317-329, 1998.
DOI : 10.1016/S0304-3975(98)00048-6
URL : http://doi.org/10.1016/s0304-3975(98)00048-6

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.
DOI : 10.1007/3-540-45949-9

M. Norrish and B. Huffman, Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ?? 1, ITP 2013, pp.133-146, 2013.
DOI : 10.1007/978-3-642-39634-2_12

C. Lawrence, J. C. Paulson, and . Blanchette, Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers, EPiC, vol.2, pp.1-11, 2010.

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
URL : http://doi.org/10.1016/0304-3975(77)90044-5

C. John and . Reynolds, Types, abstraction and parametric polymorphism, IFIP '83, pp.513-523, 1983.

M. Schmidt-schauß, Decidability of behavioural equivalence in unary PCF, Theoretical Computer Science, vol.216, issue.1-2, pp.363-373, 1999.
DOI : 10.1016/S0304-3975(98)00024-3

H. Peter and . Schmitt, A first-order theory of ordinals, TABLEAUX 2017, 2017.

G. Takeuti, Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics, 1987.

R. Thiemann, G. Allais, and J. Nagele, On the formalization of termination techniques based on multiset orderings, RTA 2012, pp.339-354, 2012.

D. Traytel, A. Popescu, and J. C. Blanchette, Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.596-605, 2012.
DOI : 10.1109/LICS.2012.75

M. Wenzel and . Isabelle, Isar?A generic framework for human-readable proof documents, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec Studies in Logic, Grammar, and Rhetoric. Uniwersytet w Bia?ymstoku, 2007.
DOI : 10.1007/3-540-48256-3_12
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.3203

H. Zankl, S. Winkler, and A. Middeldorp, Beyond polynomials and Peano arithmetic???automation of elementary and ordinal interpretations, Journal of Symbolic Computation, vol.69, pp.129-158, 2015.
DOI : 10.1016/j.jsc.2014.09.033