Constructing the real numbers in HOL

John Harrison.

Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium. Volume A-20 of IFIP Transactions A: Computer Science and Technology, North-Holland, pp. 145-164, 1992.

NB! This paper is superseded by a newer version

Abstract:

We describe a construction of the real numbers in the HOL theorem-prover by strictly definitional means using a version of Dedekind's method. We also outline the theory of mathematical analysis that has been built on top of it, and discuss current and potential applications in verification and computer algebra.

PostScript

Bibtex entry:

@INPROCEEDINGS{harrison-hol92,
        crossref        = "hol92",
        author          = "John Harrison",
        title           = "Constructing the Real Numbers in {HOL}",
        pages           = "145--164"}

@PROCEEDINGS{hol92,
        editor          = "Luc J. M. Claesen and Michael J. C. Gordon",
        booktitle       = "Proceedings of the {IFIP} {TC10/WG10.2}
                           International Workshop on Higher Order Logic Theorem
                           Proving and its Applications",
        series          = "IFIP Transactions A: Computer Science and
                           Technology",
        volume          = "A-20",
        address         = "IMEC, Leuven, Belgium",
        date            = "September 1992",
        year            = 1992,
        publisher       = "North-Holland"}