Abstract: 
We apply data refinement to implement the real numbers, where we support all
numbers in the field extension Q[sqrt(b)], i.e., all numbers of the form p +
q * sqrt(b) for rational numbers p and q and some fixed natural number b. To
this end, we also developed algorithms to precisely compute roots of a
rational number, and to perform a factorization of natural numbers which
eliminates duplicate prime factors.
Our results have been used to certify termination proofs which involve
polynomial interpretations over the reals. 
BibTeX: 
@article{Real_ImplAFP,
author = {RenĂ© Thiemann},
title = {Implementing field extensions of the form Q[sqrt(b)]},
journal = {Archive of Formal Proofs},
month = feb,
year = 2014,
note = {\url{http://isaafp.org/entries/Real_Impl.html},
Formal proof development},
ISSN = {2150914x},
}
