@article{Sturm_Tarski-AFP,
	author = {Li, Wenda},
	title = {{The Sturm--Tarski Theorem}},
	journal = {Archive of Formal Proofs},
	year = {2014},
	month = sep,
	annote = {http://isa-afp.org/entries/Sturm_Tarski.html, Formal proof development}
}

@article{Descartes_Sign_Rule-AFP,
	author  = {Manuel Eberl},
	title   = {Descartes' Rule of Signs},
	journal = {Archive of Formal Proofs},
	month   = dec,
	year    = 2015,
	note    = {\url{http://isa-afp.org/entries/Descartes_Sign_Rule.html},
	Formal proof development},
	ISSN    = {2150-914x},
}

@article{Sturm_Sequences-AFP,
	author  = {Manuel Eberl},
	title   = {Sturm's Theorem},
	journal = {Archive of Formal Proofs},
	month   = jan,
	year    = 2014,
	note    = {\url{http://isa-afp.org/entries/Sturm_Sequences.html},
	Formal proof development},
	ISSN    = {2150-914x},
}

@INPROCEEDINGS{harrison-poly,
	crossref        = "hol97",
	author          = "John Harrison",
	title           = "Verifying the accuracy of polynomial approximations
	in {HOL}",
	pages           = "137--152"}

@PROCEEDINGS{hol97,
	editor          = "Elsa L. Gunter and Amy Felty",
	booktitle       = "Theorem Proving in Higher Order Logics:
	10th International Conference, TPHOLs'97",
	series          = "Lecture Notes in Computer Science",
	volume          = 1275,
	address         = "Murray Hill, NJ",
	date            = "19--22 August 1997",
	year            = 1997,
	publisher       = "Springer-Verlag"}

@article{Narkawicz:2015do,
	author = {Narkawicz, Anthony and Mu{\~n}oz, C{\'e}sar A and Dutle, Aaron},
	title = {{Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm's and Tarski's Theorems.}},
	journal = {Journal of Automated Reasoning},
	year = {2015},
	volume = {54},
	number = {4},
	pages = {285--326}
}

@article{Mahboubi:2012gg,
	author = {Mahboubi, Assia and Cohen, Cyril},
	title = {{Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination}},
	journal = {Logical Methods in Computer Science},
	year = {2012},
	volume = {8},
	number = {1}
}

@article{li_evaluate_cauchy,
	author    = {Wenda Li and
	Lawrence C. Paulson},
	title     = {{Evaluating Winding Numbers and Counting Complex Roots through Cauchy
	Indices in Isabelle/HOL}},
	journal   = {CoRR},
	volume    = {abs/1804.03922},
	year      = {2018},
	url       = {http://arxiv.org/abs/1804.03922},
	archivePrefix = {arXiv},
	eprint    = {1804.03922},
	timestamp = {Mon, 13 Aug 2018 16:47:04 +0200},
	biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1804-03922},
	bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{Count_Complex_Roots-AFP,
	author = {Li, Wenda},
	title = {{Count the Number of Complex Roots}},
	journal = {Archive of Formal Proofs},
	year = {2017},
	month = oct,
	annote = {http://isa-afp.org/entries/Count_Complex_Roots.html, Formal proof development}
}

@book{Basu:2006bo,
	author = {Basu, Saugata and Pollack, Richard and Roy, Marie-Franco̧ise},
	title = {{Algorithms in Real Algebraic Geometry}},
	publisher = {Springer Berlin Heidelberg},
	year = {2006},
	volume = {10},
	series = {Algorithms and Computation in Mathematics},
	address = {Berlin, Heidelberg}
}

@book{Rahman:2016us,
	author = {Rahman, Qazi Ibadur and Schmeisser, Gerhard},
	title = {{Analytic Theory of Polynomials}},
	publisher = {Oxford University Press},
	year = {2002}
}








