@inproceedings{CeTA,
  author    = {R.~Thiemann and C.~Sternagel},
  title     = {Certification of Termination Proofs using \ceta},
  booktitle = {Proc.\ TPHOLs'09},
  series    = {LNCS 5674},
  year      = 2009,
  pages     = {452--468}
}

@inproceedings{NZM10,
  author      = "F.\ Neurauter and H.\ Zankl and A.\ Middeldorp",
  title       = "Monotonicity Criteria for Polynomial Interpretations over
                 the Naturals",
  booktitle   = "Proceedings of the 5th International Joint Conference on
                 Automated Reasoning",
  series      = {LNAI 6173},
  pages       = "502--517",
  year        = 2010
}

@article{Rational,
  author    = {S.\ Lucas},
  title = {Polynomials over the reals in proofs of termination: From theory to practice},
  journal = {RAIRO Theoretical Informatics and Applications},
  volume = {39},
  number = {3},
  pages = {547--586},
  year = 2005
}

@Article{Robbiano1985,
  Title                    = {{On the Theory of Graded Structures}},
  Author                   = {Lorenzo Robbiano},
  Journal                  = {Journal of Symbolic Computation},
  Year                     = {1985},
  Pages                    = {138--170},
  Volume                   = {2},
  Publisher                = {Elsevier},
  Doi                      = {10.1016/S0747-7171(86)80019-0}
}

@techreport{L79,
  author        = "D.\ Lankford",
  title         = "On Proving Term Rewriting Systems are {N}oetherian",
  institution   = "Louisiana Technical University",
  year          = "1979",
  number        = "MTP-3",
  address       = "Ruston, LA, USA"
}

@article{Sternagel2012,
  author  = {Christian Sternagel},
  title   = {{Well-Quasi-Orders}},
  journal = {Archive of Formal Proofs},
  year    = {2012},
  note    = {\url{http://isa-afp.org/entries/Well_Quasi_Orders.shtml},
            Formal proof development},
  ISSN    = {2150-914x}
}
