1. Introduction. - 1. 1 Symbolic computation. - 1. 2 Verification. - 1. 3 Higher order logic. - 1. 4 Theorem proving vs. model checking. - 1. 5 Automated vs. interactive theorem proving. - 1. 6 The real numbers. - 1. 7 Concluding remarks. - 2 Constructing the Real Numbers. - 2. 1 Properties of the real numbers. - 2. 2 Uniqueness of the real numbers. - 2. 3 Constructing the real numbers. - 2. 4 Positional expansions. - 2. 5 Cantor's method. - 2. 6 Dedekind's method. - 2. 7 What choice?. - 2. 8 Lemmas about nearly-multiplicative functions. - 2. 9 Details of the construction. - 2. 10 Adding negative numbers. - 2. 11 Handling equivalence classes. - 2. 12 Summary and related work. - 3. Formalized Analysis. - 3. 1 The rigorization and formalization of analysis. - 3. 2 Some general theories. - 3. 3 Sequences and series. - 3. 4 Limits continuity and differentiation. - 3. 5 Power series and the transcendental functions. - 3. 6 Integration. - 3. 7 Summary and related work. - 4. Explicit Calculations. - 4. 1 The need for calculation. - 4. 2 Calculation with natural numbers. - 4. 3 Calculation with integers. - 4. 4 Calculation with rationals. - 4. 5 Calculation with reals. - 4. 6 Summary and related work. - 5. A Decision Procedure for Real Algebra. - 5. 1 History and theory. - 5. 2 Real closed fields. - 5. 3 Abstract description of the algorithm. - 5. 4 The HOL Implementation. - 5. 5 Optimizing the linear case. - 5. 6 Results. - 5. 7 Summary and related work. - 6. Computer Algebra Systems. - 6. 1 Theorem provers vs. computer algebra systems. - 6. 2 Finding and checking. - 6. 3 Combining systems. - 6. 4 Applications. - 6. 5 Summary and related work. - 7. Floating Point Verification. - 7. 1 Motivation. - 7. 2 Floating point error analysis. - 7. 3 Specifying floating point operations. - 7. 4 Idealized integer and floating point operations. - 7. 5 A square root algorithm. - 7. 6 ACORDIC natural logarithm algorithm. - 7. 7 Summary and related work. - 8. Conclusions. - 8. 1 Mathematical contributions. - 8. 2 The formalization of mathematics. - 8. 3 The LCF approach to theorem proving. - 8. 4 Computer algebra systems. - 8. 5 Verification applications. - 8. 6 Concluding remarks. - A. Logical foundations of HOL. - B. Recent developments. Language: English