%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Sebastiaan Joosten at 2016-10-11 10:15:52 +0200 


%% Saved with string encoding Unicode (UTF-8) 


@string{lncs = {LNCS}}


@article{van-Hoeij:2002aa,
	Author = {{\VAN{Hoeij}{Van}{van}} Hoeij, Mark},
	Date-Added = {2016-10-11 08:11:49 +0000},
	Date-Modified = {2016-10-11 08:15:52 +0000},
	Journal = {Journal of Number theory},
	Number = {2},
	Pages = {167--189},
	Publisher = {Elsevier},
	Title = {Factoring polynomials and the knapsack problem},
	Volume = {95},
	Year = {2002}}

@manual{Mathematica11,
	Address = {Champaign, Illinois},
	Author = {Wolfram Research, Inc.},
	Date-Added = {2016-10-10 11:52:59 +0000},
	Date-Modified = {2016-10-10 11:54:29 +0000},
	Edition = {Version 11.0},
	Title = {Mathematica},
	Year = {2016}}

@inproceedings{Kobayashi2005,
	Author = {Kobayashi, Hidetune and Suzuki, Hideo and Ono, Yoko},
	Booktitle = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings},
	Date-Added = {2016-10-10 11:25:49 +0000},
	Date-Modified = {2016-10-10 11:25:49 +0000},
	Pages = {114--118},
	Title = {Formalization of {H}ensel's lemma},
	Volume = {1},
	Year = {2005}}

@techreport{Martin-Dorel:2011aa,
	Author = {Martin-Dorel, {\'E}rik},
	Date-Added = {2016-10-10 11:25:49 +0000},
	Date-Modified = {2016-10-10 11:27:34 +0000},
	Hal_Id = {ensl-00575673},
	Hal_Local_Reference = {RRLIP2011-1},
	Hal_Version = {v1},
	Institution = {ENS Lyon},
	Keywords = {Coq formal proofs ; Certifying algorithm ; Hensel's lifting ; Integral roots ; Polynomials},
	Month = Mar,
	Pdf = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-00575673/file/RRLIP2011-1.pdf},
	Title = {{Univariate and bivariate integral roots certificates based on Hensel's lifting}},
	Url = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-00575673},
	Year = {2011},
	Bdsk-Url-1 = {https://hal-ens-lyon.archives-ouvertes.fr/ensl-00575673}}

@phdthesis{kirkels2004,
	Author = {Kirkels, Bart},
	Date-Added = {2016-10-10 11:25:49 +0000},
	Date-Modified = {2016-10-10 11:25:49 +0000},
	Publisher = {Citeseer},
	School = {Radboud Universiteit Nijmegen},
	Title = {Irreducibility Certificates for Polynomials with Integer Coefficients},
	Year = {2004}}

@inproceedings{cowles2006unique,
	Author = {Cowles, John R and Gamboa, Ruben},
	Booktitle = {Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications},
	Date-Added = {2016-10-10 11:25:49 +0000},
	Date-Modified = {2016-10-10 11:25:49 +0000},
	Organization = {ACM},
	Pages = {21--27},
	Title = {Unique factorization in {ACL2}: Euclidean domains},
	Year = {2006}}

@article{mignotte1974inequality,
	Author = {Mignotte, Maurice},
	Date-Added = {2016-10-05 11:59:47 +0000},
	Date-Modified = {2016-10-05 11:59:47 +0000},
	Journal = {Mathematics of Computation},
	Number = {128},
	Pages = {1153--1157},
	Title = {An inequality about factors of polynomials},
	Volume = {28},
	Year = {1974}}

@inproceedings{WST10,
	Author = {Ren\'e Thiemann and Christian Sternagel},
	Booktitle = {WST '10},
	Note = {To appear.},
	Title = {Certified Polynomial Interpretations over Matrices and over Domains},
	Year = 2010}

@article{MatrixJAR,
	Author = {J.~Endrullis and J.~Waldmann and H.~Zantema},
	Journal = {Journal of Automated Reasoning},
	Number = {2-3},
	Pages = {195--220},
	Title = {Matrix Interpretations for Proving Termination of Term Rewriting},
	Volume = {40},
	Year = {2008}}

@inproceedings{Arctic,
	Author = {A.\@ Koprowski and J.\@ Waldmann},
	Booktitle = {RTA'08},
	Pages = {202--216},
	Series = {LNCS},
	Title = {Arctic Termination {\ldots} Below Zero},
	Volume = 5117,
	Year = {2008}}

@inproceedings{CeTA,
	Author = {R.~Thiemann and C.~Sternagel},
	Booktitle = {TPHOLs'09},
	Pages = {452--468},
	Series = {LNCS},
	Title = {Certification of Termination Proofs using \ceta},
	Volume = 5674,
	Year = 2009}

@inproceedings{CeTAcomplexity,
	Author = {M.~Avanzini and C.~Sternagel and R.~Thiemann},
	Booktitle = {{RTA} 2015},
	Pages = {23--39},
	Series = {LIPIcs 36},
	Title = {Certification of Complexity Proofs using \ceta},
	Year = {2015}}

@book{PO07,
	Author = {Piziak, Robert and Odell, Patrick L},
	Publisher = {CRC Press},
	Title = {Matrix theory: from generalized inverses to {J}ordan form},
	Year = {2007}}

@article{Containers-AFP,
	Author = {Andreas Lochbihler},
	Journal = {Archive of Formal Proofs},
	Month = apr,
	Oissn = {2150-914x},
	Title = {Light-weight Containers},
	Url = {https://isa-afp.org/entries/Containers.shtml},
	Year = 2013,
	Bdsk-Url-1 = {https://isa-afp.org/entries/Containers.shtml}}

@article{Gauss-Jordan-AFP,
	Author = {Jose Divas\'on and Jes{\'u}s Aransay},
	Journal = {Archive of Formal Proofs},
	Month = sep,
	Oissn = {2150-914x},
	Title = {{G}auss-{J}ordan Algorithm and Its Applications},
	Url = {https://isa-afp.org/entries/Gauss_Jordan.shtml},
	Year = 2014,
	Bdsk-Url-1 = {https://isa-afp.org/entries/Gauss_Jordan.shtml}}

@inproceedings{DA13,
	Author = {Jose Divas\'on and Jes{\'u}s Aransay},
	Booktitle = {LOPSTR 2013},
	Series = {LNCS},
	Title = {Formalization and execution of Linear Algebra: from theorems to algorithms},
	Volume = 8901,
	Year = 2013}

@article{QR-AFP,
	Author = {Jose Divas{\'{o}}n and Jes{\'{u}}s Aransay},
	Journal = {Archive of Formal Proofs},
	Title = {{QR} Decomposition},
	Url = {https://isa-afp.org/entries/QR_Decomposition.shtml},
	Year = {2015},
	Bdsk-Url-1 = {https://isa-afp.org/entries/QR_Decomposition.shtml}}

@article{Matrix-AFP,
	Author = {Christian Sternagel and Rene Thiemann},
	Journal = {Archive of Formal Proofs},
	Month = jun,
	Oissn = {2150-914x},
	Title = {Executable Matrix Operations on Matrices of Arbitrary Dimensions},
	Url = {https://isa-afp.org/entries/Matrix.shtml},
	Year = 2010,
	Bdsk-Url-1 = {https://isa-afp.org/entries/Matrix.shtml}}

@book{AlgNumbers,
	Author = {Bhubaneswar Mishra},
	Bibsource = {dblp computer science bibliography, http://dblp.org},
	Biburl = {http://dblp.uni-trier.de/rec/bib/books/daglib/0071396},
	Isbn = {978-3-540-94090-6},
	Opt_Doi = {10.1007/978-1-4612-4344-1},
	Opt_Url = {https://doi.org/10.1007/978-1-4612-4344-1},
	Publisher = {Springer},
	Series = {Texts and Monographs in Computer Science},
	Timestamp = {Mon, 12 Jan 2015 17:10:19 +0100},
	Title = {Algorithmic Algebra},
	Year = {1993}}

@book{Knuth,
	Author = {Donald E. Knuth},
	Bibsource = {dblp computer science bibliography, http://dblp.org},
	Biburl = {http://dblp.uni-trier.de/rec/bib/books/aw/Knuth81},
	Isbn = {0-201-03822-6},
	Publisher = {Addison-Wesley},
	Timestamp = {Thu, 03 Jan 2002 11:51:07 +0100},
	Title = {The Art of Computer Programming, Volume {II:} Seminumerical Algorithms, 2nd Edition},
	Year = {1981}}

@inproceedings{NZM10,
	Author = {Friedrich Neurauter and Harald Zankl and Aart Middeldorp},
	Booktitle = {LPAR-17},
	Opdoi = {10.1007/978-3-642-16242-8_39},
	Pages = {550--564},
	Series = {LNCS},
	Title = {Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting},
	Volume = 6397,
	Year = {2010}}

@inproceedings{MSW08,
	Author = {Georg Moser and Andreas Schnabl and Johannes Waldmann},
	Booktitle = {{FSTTCS} 2008},
	Opdoi = {10.4230/LIPIcs.FSTTCS.2008.1762},
	Pages = {304--315},
	Series = {LIPIcs},
	Title = {Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations},
	Volume = 2,
	Year = {2008}}

@inproceedings{MMNWZ11,
	Author = {Aart Middeldorp and Georg Moser and Friedrich Neurauter and Johannes Waldmann and Harald Zankl},
	Booktitle = {CAI 2011},
	Opdoi = {10.1007/978-3-642-21493-6_1},
	Pages = {1--20},
	Series = {LNCS},
	Title = {Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems},
	Volume = 6742,
	Year = {2011}}

@article{Strassen,
	Author = {Volker Strassen},
	Issue = 4,
	Journal = {Numerische Mathematik},
	Opdoi = {10.1007/BF02165411},
	Pages = {354--356},
	Title = {Gaussian elimination is not optimal},
	Volume = 13,
	Year = {1969}}

@book{JNF,
	Author = {Camille Jordan},
	Publisher = {Gauthier-Villars},
	Title = {Trait{\'e} des substitutions et des {\'e}quations alg{\'e}briques},
	Year = 1870}

@book{Isabelle,
	Author = {T.~Nipkow and L.C.~Paulson and M.~Wenzel},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {{Isabelle/HOL} -- A Proof Assistant for Higher-Order Logic},
	Volume = 2283,
	Year = 2002}

@inproceedings{Yun,
	Author = {David Yun},
	Booktitle = {the third ACM symposium on Symbolic and Algebraic Computation},
	Opdoi = {10.1145/800205.806320},
	Oppublisher = {ACM},
	Pages = {26-35},
	Title = {On square-free decomposition algorithms},
	Year = {1976}}

@article{HMA,
	Author = {John Harrison},
	Journal = {J. Autom. Reasoning},
	Number = {2},
	Opdoi = {10.1007/s10817-012-9250-9},
	Pages = {173--190},
	Title = {The {HOL} Light Theory of {E}uclidean Space},
	Volume = {50},
	Year = {2013}}

@inproceedings{Sturm-AFP,
	Author = {Manuel Eberl},
	Booktitle = {CPP 2015},
	Opdoi = {2676724.2693166},
	Pages = {75-83},
	Publisher = {ACM},
	Title = {A Decision Procedure for Univariate Real Polynomials in {I}sabelle/{HOL}},
	Year = 2015}

@article{SturmLinalg,
	Author = {J. C. F. Sturm},
	Journal = {Bulletin des Sciences de F{\'e}russac},
	Pages = {419--425},
	Title = {M{\'e}moire sur la r{\'e}solution des {\'e}quations num{\'e}riques},
	Volume = 11,
	Year = 1829}

@article{Real-AFP,
	Author = {Ren{\'e} Thiemann},
	Journal = {Archive of Formal Proofs},
	Month = feb,
	Oissn = {2150-914x},
	Title = {Implementing field extensions of the form {$\mathbb{Q}[\sqrt{b}]$}},
	Url = {https://isa-afp.org/entries/Real_Impl.shtml},
	Year = 2014,
	Bdsk-Url-1 = {https://isa-afp.org/entries/Real_Impl.shtml}}

@inproceedings{realMatrix,
	Author = {Christian Sternagel and Ren{\'e} Thiemann},
	Booktitle = {RTA-TLCA 2014},
	Opdoi = {10.1007/978-3-319-08587-6_13},
	Opeditor = {Gilles Dowek},
	Pages = {441--455},
	Series = {LNCS (ARCoSS)},
	Title = {Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs},
	Volume = 8560,
	Year = 2014}

@inproceedings{lifting,
	Author = {B. Huffman and O. Kun\v{c}ar},
	Booktitle = {CPP 2013},
	Opdoi = {10.1007/978-3-319-03545-1_9},
	Oppublisher = {Springer},
	Pages = {131--146},
	Series = {LNCS},
	Title = {Lifting and Transfer: A Modular Design for Quotients in {I}sabelle/{HOL}},
	Volume = 8307,
	Year = 2013}

@article{JNF-AFP,
	Author = {Ren{\'e} Thiemann and Akihisa Yamada},
	Journal = {Archive of Formal Proofs},
	Month = aug,
	Oissn = {2150-914x},
	Title = {Matrices, {J}ordan Normal Forms, and Spectral Radius Theory},
	Url = {https://isa-afp.org/entries/Jordan_Normal_Form.shtml},
	Year = 2015,
	Bdsk-Url-1 = {https://isa-afp.org/entries/Jordan_Normal_Form.shtml}}

@article{Vector-Space-AFP,
	Author = {Holden Lee},
	Journal = {Archive of Formal Proofs},
	Title = {Vector Spaces},
	Url = {http://www.isa-afp.org/entries/VectorSpace.shtml},
	Year = {2014},
	Bdsk-Url-1 = {http://www.isa-afp.org/entries/VectorSpace.shtml}}

@inproceedings{HOLAlgebra,
	Author = {Clemens Ballarin},
	Booktitle = {CICM Workshops 2013},
	Oppublisher = {CEUR-WS.org},
	Series = {{CEUR} Workshop Proceedings},
	Title = {Reading an algebra textbook},
	Volume = {1010},
	Year = {2013}}

@inproceedings{W10,
	Address = {Dagstuhl, Germany},
	Author = {Johannes Waldmann},
	Booktitle = {RTA 2010},
	Oisbn = {978-3-939897-18-7},
	Oissn = {1868-8969},
	Opdoi = {10.4230/LIPIcs.RTA.2010.357},
	Opeditor = {Christopher Lynch},
	Oppublisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
	Pages = {357--372},
	Series = {Leibniz International Proceedings in Informatics (LIPIcs)},
	Title = {{Polynomially Bounded Matrix Interpretations}},
	Volume = {6},
	Year = {2010}}

@inproceedings{aprove,
	Author = {J{\"u}rgen Giesl and Marc Brockschmidt and Fabian Emmes and Florian Frohn and Carsten Fuhs and Carsten Otto and Martin Pl{\"u}cker and Peter Schneider-Kamp and Thomas Str{\"o}der and Stephanie Swiderski and Ren{\'e} Thiemann},
	Booktitle = {IJCAR 2014},
	Opdoi = {10.1007/978-3-319-08587-6_13},
	Opeditor = {St{\'e}phane Demri and Deepak Kapur and Christoph Weidenbach},
	Pages = {184--191},
	Series = {LNCS},
	Title = {Proving Termination of Programs Automatically with {AProVE}},
	Volume = 8562,
	Year = 2014}

@inproceedings{tct,
	Author = {Martin Avanzini and Georg Moser},
	Booktitle = {RTA 2013},
	Opdoi = {10.4230/LIPIcs.RTA.2013.71},
	Opeditor = {Femke van Raamsdonk},
	Pages = {71--80},
	Series = {LIPIcs},
	Title = {{T}yrolean {C}omplexity {T}ool: Features and Usage},
	Volume = 21,
	Year = 2013}

@article{cat,
	Author = {Harald Zankl and Martin Korp},
	Journal = {Logical Methods in Computer Science},
	Number = {1:19},
	Pages = {1--34},
	Title = {Modular Complexity Analysis for Term Rewriting},
	Volume = 10,
	Year = 2014}

@inproceedings{TermComp15,
	Author = {J{\"{u}}rgen Giesl and Fr{\'{e}}d{\'{e}}ric Mesnard and Albert Rubio and Ren{\'{e}} Thiemann and Johannes Waldmann},
	Booktitle = {CADE-25},
	Opdoi = {10.1007/978-3-319-21401-6_6},
	Opeditor = {Amy P. Felty and Aart Middeldorp},
	Oppublisher = {Springer},
	Pages = {105--108},
	Series = {LNCS},
	Title = {Termination Competition ({termCOMP} 2015)},
	Volume = {9195},
	Year = {2015}}

@article{Berlekamp,
	Author = {Elwyn R. Berlekamp},
	Journal = {Bell System Technical Journal},
	Pages = {1853--1859},
	Title = {Factoring Polynomials Over Finite Fields},
	Volume = 46,
	Year = 1967}

@article{Berlekamp70,
	Author = {E.R. Berlekamp},
	Journal = {Math.\@ Comp.\@},
	Number = 24,
	Pages = {713-735},
	Year = 1970}

@book{Hensel,
	Author = {Kurt Hensel},
	Publisher = {Teubner, Leipzig},
	Title = {Theorie der Algebraischen Zahlen},
	Year = 1908}

@inproceedings{ThiemannY16,
	Author = {Ren{\'e} Thiemann and Akihisa Yamada},
	Booktitle = {CPP~2016},
	Opeditor = {Jeremy Avigad and Adam Chlipala},
	Pages = {88--99},
	Publisher = {ACM},
	Title = {Formalizing {J}ordan normal forms in {I}sabelle/{HOL}},
	Year = 2016}

@inproceedings{LiP16,
	Author = {Wenda Li and Lawrence C. Paulson},
	Booktitle = {CPP~2016},
	Opeditor = {Jeremy Avigad and Adam Chlipala},
	Pages = {66--75},
	Publisher = {ACM},
	Title = {A modular, efficient formalisation of real algebraic numbers},
	Year = 2016}

@inproceedings{CohenD16,
	Author = {Cyril Cohen and Boris Djalal},
	Booktitle = {CPP~2016},
	Opeditor = {Jeremy Avigad and Adam Chlipala},
	Pages = {100--109},
	Publisher = {ACM},
	Title = {Formalization of a {N}ewton series representation of polynomials},
	Year = {2016}}

@inproceedings{Cohen12,
	Author = {Cyril Cohen},
	Booktitle = {ITP~2012},
	Opeditor = {Lennart Beringer and Amy P. Felty},
	Optpublisher = {Springer},
	Pages = {67--82},
	Series = lncs,
	Title = {Construction of Real Algebraic Numbers in {C}oq},
	Volume = {7406},
	Year = {2012}}

@inproceedings{DataRefinement,
	Author = {Florian Haftmann and Alexander Krauss and Ondrej Kun\v{c}ar and Tobias Nipkow},
	Booktitle = {ITP~2013},
	Optpublisher = {Springer},
	Pages = {100--115},
	Series = lncs,
	Title = {Data Refinement in {I}sabelle/{HOL}},
	Volume = {7998},
	Year = {2013}}

@unpublished{Chen13,
	Author = {Ruiyuan R. Chen},
	Note = {Available at \url{http://www.math.ubc.ca/~reichst/423-project-subresultant.pdf}},
	Title = {The Subresultant Polynomial Remainder Sequence Algorithm},
	Year = 2013}

@article{Brown,
	Author = {W. S. Brown},
	Journal = {{ACM} Trans. Math. Softw.},
	Number = {3},
	Pages = {237--249},
	Title = {The Subresultant {PRS} Algorithm},
	Volume = {4},
	Year = {1978}}

@book{Polynomials,
	Author = {Victor V. Prasolov},
	Publisher = {Springer},
	Title = {Polynomials},
	Year = 2004}

@inproceedings{partial_function,
	Author = {Alexander Krauss},
	Booktitle = {PAR 2010},
	Opteditor = {Ana Bove and Ekaterina Komendantskaya and Milad Niqui},
	Optnote = {\doi{10.4204/EPTCS.43.1}},
	Optshorteditor = {Ana Bove and others},
	Pages = {1--13},
	Series = {EPTCS},
	Title = {Recursive Definitions of Monadic Functions},
	Volume = {43},
	Year = 2010}

@article{Collins67,
	Author = {G. E. Collins},
	Journal = {Journal of the ACM},
	Pages = {128-142},
	Title = {Subresultants and reduced polynomial remainder sequences},
	Volume = 14,
	Year = 1967}

@article{Martin-Dorel2015,
	Author = {Martin-Dorel, {\'E}rik and Hanrot, Guillaume and Mayero, Micaela and Th{\'e}ry, Laurent},
	Journal = {Journal of Automated Reasoning},
	Number = {1},
	Pages = {1--29},
	Title = {Formally Verified Certificate Checkers for Hardest-to-Round Computation},
	Volume = {54},
	Year = {2015}}

@inproceedings{McLaughlin2005,
	Author = {McLaughlin, Sean and Harrison, John},
	Booktitle = {CADE-20},
	Editor = {Nieuwenhuis, Robert},
	Pages = {295--314},
	Series = {LNCS},
	Title = {A Proof-Producing Decision Procedure for Real Arithmetic},
	Volume = 3632,
	Year = {2005}}

@inproceedings{Mahboubi2006,
	Author = {Mahboubi, Assia},
	Booktitle = {IJCAR 2006},
	Pages = {438--452},
	Series = {LNCS},
	Title = {Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials},
	Volume = 4130,
	Year = {2006}}

@article{CohenM2012,
	Author = {Cohen, Cyril and Mahboubi, Assia},
	Journal = {Logical Methods in Computer Science},
	Number = {1:02},
	Pages = {1-40},
	Title = {Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination},
	Volume = {8},
	Year = {2012}}

@inproceedings{TY16,
	Author = {Ren{\'e} Thiemann and Akihisa Yamada},
	Booktitle = {ITP 2016},
	Pages = {391-408},
	Series = {LNCS},
	Title = {Algebraic Numbers in {I}sabelle/{HOL}},
	Volume = {9807},
	Year = {2016}}

@inproceedings{KP16,
	Author = {Ond{\v r}ej Kun{\v c}ar and Andrei Popescu},
	Booktitle = {ITP 2016},
	Pages = {200-218},
	Series = {LNCS},
	Title = {From Types to Sets by Local Type Definitions in Higher-Order Logic},
	Volume = {9807},
	Year = {2016}}

@article{CZ81,
	Author = {David G. Cantor and Hans Zassenhaus},
	Journal = {Math.\@ Comput.\@},
	Number = 154,
	Pages = {587-592},
	Title = {A New Algorithm for Factoring Polynomials Over Finite Fields},
	Volume = 36,
	Year = 1981}

@inproceedings{codegen,
	Author = {Florian Haftmann and Tobias Nipkow},
	Booktitle = {FLOPS 2010},
	Opteditor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
	Optnote = {\doi{10.1007/978-3-642-12251-4_9}},
	Pages = {103--117},
	Series = {LNCS},
	Title = {Code Generation via Higher-Order Rewrite Systems},
	Volume = 6009,
	Year = 2010}

@inproceedings{NoCoqFactorization,
	Author = {Gilles Barthe and Benjamin Gr{\'{e}}goire and Sylvain Heraud and Federico Olmedo and Santiago Zanella B{\'{e}}guelin},
	Booktitle = {{POST} 2012},
	Pages = {209--228},
	Series = {LNCS},
	Title = {Verified Indifferentiable Hashing into Elliptic Curves},
	Volume = {7215},
	Year = {2012}}

@article{MiolaY74,
author={Miola, Alfonso and David Y.Y. Yun},
title="Computational aspects of {H}ensel-type univariate polynomial greatest common divisor algorithms",
journal={ACM SIGSAM Bulletin},
volume=8,
number=3,
pages={46-54},
year=1974
}

@article{Zassenhaus69,
author={Zassenhaus, Hans},
title="On {H}ensel factorization, {I}",
journal="Journal of Number Theory",
volume=1,
number=3,
pages={291-311},
year=1969
}
