A verified decision procedure for univariate real arithmetic with the BKR algorithm

@inproceedings{DBLP:conf/itp/CordwellTP21,
	pdf = {https://drops.dagstuhl.de/opus/volltexte/2021/13909/pdf/LIPIcs-ITP-2021-14.pdf},
	slides = {pub/QE-BKR-slides.pdf},
	study = {http://isa-afp.org/entries/BenOr_Kozen_Reif.html},
	author = {['Katherine Cordwell', 'Yong Kiam Tan', 'André Platzer']},
	editor = {['Liron Cohen', 'Cezary Kaliszyk']},
	title = {A Verified Decision Procedure for Univariate Real Arithmetic with
               the BKR Algorithm},
	booktitle = {12th International Conference on Interactive Theorem Proving, ITP
               2021, June 29 to July 1, 2021, Rome, Italy},
	series = {LIPIcs},
	volume = {193},
	pages = {14:1–14:20},
	publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
	year = {2021},
	doi = {10.4230/LIPIcs.ITP.2021.14},
	biburl = {https://dblp.org/rec/conf/itp/CordwellTP21.bib}
}