Book: "Theorem Proving with the Real Numbers"

[While not connected with the contemporary lines of research in type theory,
 the following book discusses the formalization of some non-trivial classical
 mathematics in simple type theory. It will be of particular relevance to
 those interested in mechanized theorem proving, and in how informal
 mathematics fits into formal systems.]

People interested in the formalization of mathematics, computer-aided
verification and related fields may like to know that a revised version
of my PhD thesis is now available from Springer-Verlag. The following
information is taken from the publisher's Web page


You can conveniently order the book directly from that page.

    Theorem Proving with the Real Numbers

    John Harrison

    Theorem Proving with the Real Numbers discusses the formal development
    of classical mathematics using a computer. It combines traditional
    lines of research in theorem proving and computer algebra and shows
    the usefulness of real numbers in verification. This book aims to show
    that a theory of real numbers is useful in practice as well as
    theoretically interesting, and that the 'LCF' style of theorem proving
    is well suited to the kind of work described.

    CONTENTS: Introduction - Constructing the Real Numbers - Formalized
    Analysis - Explicit Calculations - A Decision Procedure for Real
    Algebra - Computer Algebra Systems - Floating Point Verification -
    Conclusions - Logical Foundations of HOL - Recent Developments -
    Bibliography - Index

    200 pages 234 x 156mm hardcover 1998 3-540-76256-6 #40.00

Some of the theories described are distributed in the examples directory
of the HOL Light prover, available via the Web page


If people are interested, I can make the rest of the HOL code available

John Harrison (http://www.cl.cam.ac.uk/users/jrh).