@inproceedings{WST10,
  author    = {Ren\'e Thiemann and Christian Sternagel},
  title     = {Certified Polynomial Interpretations over Matrices and over Domains}, 
  year      = 2010,
  booktitle = {Proc.\ WST '10},
  note = "To appear."
}

@Article{MatrixJAR,
  author =       {J.~Endrullis and J.~Waldmann and H.~Zantema},
  title =        {{Matrix Interpretations for Proving Termination of Term Rewriting}},
  journal =      {Journal of Automated Reasoning},
  year =         {2008},
  OPTkey =       {},
  volume =       {40},
  number =       {2-3},
  pages =        {195--220},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}

@inproceedings{Arctic,
  author    = {A.\ Koprowski and J.\ Waldmann},
  title     = {Arctic Termination {\ldots} Below Zero},
  booktitle = {Proc.\ RTA'08},
  year      = {2008},
  pages     = {202--216},
  series = "LNCS 5117"
}

@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{CeTAcomplexity,
  author    = {M.~Avanzini and C.~Sternagel and R.~Thiemann},
  title     = {Certification of Complexity Proofs using \ceta},
  booktitle = {Proc.\ {RTA} 2015},
  series    = {LIPIcs 36},
  pages     = {23--39},
  year      = {2015}
}

@book{PO07,
  title={Matrix theory: from generalized inverses to {J}ordan form},
  author={Piziak, Robert and Odell, Patrick L},
  year={2007},
  publisher={CRC Press}
}

@article{Containers-AFP,
  author  = {Andreas Lochbihler},
  title   = {Light-weight Containers},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2013,
  note    = {\url{http://isa-afp.org/entries/Containers.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Gauss_Jordan-AFP,
  author  = {Jose Divas\'on and Jesus Aransay},
  title   = {Gauss-Jordan Algorithm and Its Applications},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Gauss_Jordan.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Matrix-AFP,
  author  = {Christian Sternagel and Rene Thiemann},
  title   = {Executable Matrix Operations on Matrices of Arbitrary Dimensions},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2010,
  note    = {\url{http://isa-afp.org/entries/Matrix.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@book{AlgNumbers,
  author    = {Bhubaneswar Mishra},
  title     = {Algorithmic Algebra},
  series    = {Texts and Monographs in Computer Science},
  publisher = {Springer},
  year      = {1993},
  url       = {https://doi.org/10.1007/978-1-4612-4344-1},
  doi       = {10.1007/978-1-4612-4344-1},
  isbn      = {978-3-540-94090-6},
  timestamp = {Mon, 12 Jan 2015 17:10:19 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/books/daglib/0071396},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@book{Knuth,
  author    = {Donald E. Knuth},
  title     = {The Art of Computer Programming, Volume {II:} Seminumerical Algorithms,
               2nd Edition},
  publisher = {Addison-Wesley},
  year      = {1981},
  isbn      = {0-201-03822-6},
  timestamp = {Thu, 03 Jan 2002 11:51:07 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/books/aw/Knuth81},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@article{JNF-AFP,
  author    = {Ren{\'{e}} Thiemann and
               Akihisa Yamada},
  title     = {Matrices, {J}ordan Normal Forms, and Spectral Radius Theory},
  journal   = {Archive of Formal Proofs},
  volume    = {2015},
  year      = {2015},
  url       = {http://isa-afp.org/entries/Jordan_Normal_Form.shtml},
  timestamp = {Fri, 02 Oct 2015 13:06:45 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/afp/ThiemannY15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article{Real-AFP,
  author    = {Ren{\'{e}} Thiemann},
  title     = {Implementing field extensions of the form $\rats[\sqrt b]$},
  journal   = {Archive of Formal Proofs},
  volume    = {2014},
  year      = {2014},
  url       = {http://isa-afp.org/entries/Real_Impl.shtml},
  timestamp = {Mon, 24 Mar 2014 12:06:18 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/afp/Thiemann14},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{Sturm-AFP,
  author  = {Manuel Eberl},
  title   = {A Decision Procedure for Univariate Real Polynomials in {I}sabelle/{HOL}},
  booktitle = {Proc.\@ CPP 2015},
  pages = {75-83},
  publisher = {ACM},
  year = 2015,
  OPdoi = {2676724.2693166},
}

@inproceedings{Yun,
  author = {David Yun},
  booktitle = {Proc.\@ the third ACM symposium on Symbolic and Algebraic Computation},
  title = {On square-free decomposition algorithms},
  pages = {26-35},
  year = {1976},
  OPpublisher = {ACM},
  OPdoi = {10.1145/800205.806320}
}

@article{Berlekamp,
  author = {Elwyn R. Berlekamp},
  title = {Factoring Polynomials Over Finite Fields},
  journal = {Bell System Technical Journal},
  volume = 46,
  year = 1976,
  pages = {1853--1859}
}

@book{Hensel,
  author = {Kurt Hensel},
  title = {Theorie der Algebraischen Zahlen},
  publisher = "Teubner, Leipzig",
  year = 1908
}
