Constructing the real numbers in HOL

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.

PostScript

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"}