John Harrison: Papers

The real numbers in theorem proving

A HOL Theory of Euclidean space.

Proceedings of TPHOLs 2005: 18th International Conference on Theorem Proving in Higher Order Logics. Springer LNCS 3603, pp. 114-129, 2005.

A Proof-Producing Decision Procedure for Real Arithmetic.

Proceedings of CADE-20: 20th International Conference on Automated Deduction. Springer LNCS 3632, pp. 295-314, 2005.

Constructing the Real Numbers in HOL.

Formal Methods in System Design, vol. 5, pp. 35-59, 1994.

Theorem proving with the real numbers (my PhD thesis).

Technical Report number 408, University of Cambridge Computer Laboratory, December 1996.

Floating point verification

Floating-Point Verification using Theorem Proving.

Proceedings of SFM 2006, the 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems. Springer LNCS 2965, pp. 211-242, 2006.

Floating-Point Verification.

Proceedings of FM 2005: International Symposium of Formal Methods Europe (Industry Day). Springer LNCS 3582, pp. 529-532, 2005.

Isolating critical cases for reciprocals using integer factorization .

Proceedings of the 16th IEEE Symposium on Computer Arithmetic, IEEE Computer Society Press, pp. 148-157, 2003.

Formal verification of square root algorithms.

Formal Methods in System Design, vol. 22, pp. 143-153, 2003.

Formal verification of floating point trigonometric functions.

Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design, FMCAD 2000. Springer LNCS 1954, pp. 217-233, 2000.

Formal verification of IA-64 division algorithms.

Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2000. Springer LNCS 1869, pp. 234-251, 2000.

A Machine-Checked Theory of Floating Point Arithmetic.

Proceedings of the 1999 International Conference on Theorem Proving in Higher Order Logics, TPHOLs'99. Springer LNCS 1690, pp. 113-130, 1999.

Floating point verification in HOL Light: the exponential function.

Technical Report number 428, University of Cambridge Computer Laboratory, June 1997.

Verifying the accuracy of polynomial approximations in HOL.

Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'97, Springer LNCS 1275, pp. 137-152.

General philosophy of theorem proving and formalization

Metatheory and Reflection in Theorem Proving: A Survey and Critique.

Technical Report CRC-053, SRI International Cambridge Computer Science Research Centre, 1995.

Formalized Mathematics.

TUCS Technical Report number 36, August 1996.

Proof Style.

Proceedings of BRA Types workshop (Aussois), 1996. Springer LNCS 1512, pp. 154-172.

First Order Logic in Practice.

Proceedings of FTP'97.

Specific work in LCF-style theorem proving

Towards self-verification of HOL Light.

Proceedings of IJCAR 2006, the third International Joint Conference on Automated Reasoning. Springer LNCS 4130, pp. 177-191, 2006.

Complex quantifier elimination in HOL.

Supplementary proceedings of the 2001 International Conference on Theorem Proving in Higher Order Logics, pp. 159-174, 2001.

Formalizing Dijkstra.

Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 171-188, 1998.

Formalizing Basic First Order Model Theory.

Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170, 1998.

Binary Decision Diagrams as a HOL Derived Rule.

The Computer Journal, vol. 38, pp. 162-170, 1995.

A Mizar Mode for HOL.

Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'96, Springer LNCS 1125, pp. 203-220, 1996.

Stålmarck's algorithm as a HOL derived rule.

Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'96, Springer LNCS 1125, pp. 221-234, 1996.

A Sceptic's Approach to Combining HOL and Maple.

(With Laurent Théry.) Journal of Automated Reasoning, vol. 21, pp. 279-294, 1998.

First order automated theorem proving

Optimizing Proof Search in Model Elimination.

Proceedings of the 13th International Conference on Automated Deduction (CADE'13), Springer LNCS 1104, pp. 313-327, 1996. Longer version available as TUCS Technical Report number 6.

Construction of LCF-style theorem provers

A Reference Version of HOL.

(With Konrad Slind.) Poster session of 1994 HOL Users Meeting; only published in supplementary proceedings.

HOL Done Right.

Unpublished draft, 21st August 1995.

HOL Light: A Tutorial Introduction.

Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), Springer LNCS 1166, pp. 265-269, 1996.

Embedding formal languages in theorem provers

Experience with embedding hardware description languages in HOL .

(With Richard Boulton, Andrew Gordon, Mike Gordon, John Herbert and John Van Tassel.) Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen. North-Holland, IFIP Transactions A-10, pp. 129-156, 1993.