@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher=Springer,series=LNCS,volume=2283,year=2002,
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}

@PhdThesis{cohen_phd,
  Title                    = {{Formalized algebraic numbers: construction and
 first-order theory}},
  Author                   = {Cohen, Cyril},
  School                   = {{\'E}cole polytechnique},
  Year                     = {2012},
  Month                    = {{Nov}},

  Affiliation              = {Laboratoire d'informatique de l'{\'E}cole
 polytechnique - LIX, INRIA Saclay - Ile de France,
 Microsoft Research - Inria Joint Centre},
  File                     = {thesis.pdf:http\://perso.crans.org/cohen/papers/thesis.pdf:PDF},
  Keywords                 = {Coq; Formal proofs; Formalization of mathematics;
 Small scale reflection; Algebraic numbers;
 Constructive mathematics; Quantifier elimination;
 Real numbers},
  Language                 = {English}
}

@Book{Basu:2006:ARA:1197095,
  Title                    = {Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics)},
  Author                   = {Basu, Saugata and Pollack, Richard and Roy, Marie-Fran\c{c}oise},
  Publisher                = {Springer-Verlag New York, Inc.},
  Year                     = {2006},

  Address                  = {Secaucus, NJ, USA},

  ISBN                     = {3540330984}
}

@inproceedings{Li_CPP_16,
	author = {Li, Wenda and Paulson, Lawrence C.},
	title = {A Modular, Efficient Formalisation of Real Algebraic Numbers},
	booktitle = {Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs},
	series = {CPP 2016},
	year = {2016},
	isbn = {978-1-4503-4127-1},
	location = {St. Petersburg, FL, USA},
	pages = {66--75},
	numpages = {10},
	url = {http://doi.acm.org/10.1145/2854065.2854074},
	doi = {10.1145/2854065.2854074},
	acmid = {2854074},
	publisher = {ACM},
	address = {New York, NY, USA},
	keywords = {Decision procedure, Isabelle/HOL, Real algebraic geometry},
} 

@article{Algebraic_Numbers-AFP,
	author  = {René Thiemann and Akihisa Yamada},
	title   = {Algebraic Numbers in Isabelle/HOL},
	journal = {Archive of Formal Proofs},
	month   = dec,
	year    = 2015,
	note    = {\url{http://isa-afp.org/entries/Algebraic_Numbers.shtml},
	Formal proof development},
	ISSN    = {2150-914x},
}

@article{Sturm_Tarski-AFP,
	author  = {Wenda Li},
	title   = {The Sturm--Tarski Theorem},
	journal = {Archive of Formal Proofs},
	month   = sep,
	year    = 2014,
	note    = {\url{http://isa-afp.org/entries/Sturm_Tarski.shtml},
	Formal proof development},
	ISSN    = {2150-914x},
}

@book{rahman2002analytic,
	title={Analytic theory of polynomials},
	author={Rahman, Qazi Ibadur and Schmeisser, Gerhard},
	number={26},
	year={2002},
	publisher={Oxford University Press}
}

@article{eisermann2012fundamental,
	title={The fundamental theorem of algebra made effective: An elementary real-algebraic proof via {S}turm chains},
	author={Eisermann, Michael},
	journal={American Mathematical Monthly},
	volume={119},
	number={9},
	pages={715--752},
	year={2012},
	publisher={Mathematical Association of America}
}
