John Harrison.
Formal Methods in System Design, vol. 5, pp. 35-59, 1994.
Abstract:
This paper describes a construction of the real numbers in the HOL
theorem-prover by strictly definitional means using a version of Dedekind's
method. It also outlines the theory of mathematical analysis that has been
built on top of it and discusses current and potential applications in
verification and computer algebra.
Bibtex entry:
@ARTICLE{harrison-fmsd94,
author = "John Harrison",
title = "Constructing the Real Numbers in {HOL}",
journal = "Formal Methods in System Design",
year = 1994,
volume = 5,
pages = "35--59"}