John Harrison: Papers

Specific work in LCF-style theorem proving

A formalized proof of Dirichlet's theorem on primes in arithmetic progression.

Journal of Formalized Reasoning, vol. 2, no. 1, pp. 63-83, 2009.

Formalizing an analytic proof of the Prime Number Theorem.

Journal of Automated Reasoning, vol. 43, pp. 243-261, 2009.

Without Loss of Generality.

Proceedings of TPHOLs 2009, Springer LNCS 5674, pp. 43-59, 2009.

Formalizing an analytic proof of the Prime Number Theorem (extended abstract).

Participant's proceedings of TTVSI Festschrift in honour of Mike Gordon's 60th birthday, 2008.

Verifying nonlinear real formulas via sums of squares.

Proceedings of TPHOLs 2007, Springer LNCS vol. 4732, pp. 102-118, 2007.

Automating elementary number-theoretic proofs using Gröbner bases.

Proceedings of CADE 21, Springer LNCS vol. 4603, pp. 51--66, 2007.

Formalizing basic complex analysis.

Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric vol. 10(23), pp. 151-165, 2007.

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.

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

Formal Proof -- Theory and Practice.

Notices of the American Mathematical Society, vol. 55, pp. 1395-1406, 2008.

A short survey of automated reasoning.

Proceedings of AB 2007, Springer LNCS vol. 4545, pp. 334-349, 2007.

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.

Pure logic and automated theorem proving

Some new results on decidability for elementary algebra and geometry.

(With Robert M. Solovay and R.D. Arthan.) ArXiV preprint 0904.3482, submitted to Annals of Pure and Applied Logic, 2009.

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

HOL Light: An Overview.

Proceedings of TPHOLs 2009, Springer LNCS 5674, pp. 60-66.

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.

Computer arithmetic

Decimal Transcendentals via Binary.

Proceedings of ARITH-19, IEEE Computer Society Press, 2009, pp. 187-194.

Fast and Accurate Bessel Function Computation.

Proceedings of ARITH-19, IEEE Computer Society Press, 2009, pp. 104-113.

A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format.

(With Marius Cornea, Cristina Anderson, Ping Tak Peter Tang, Eric Schneider and Evgeny Gvozdev.) IEEE Transactions on Computers, vol. 58, pp. 148--162, 2009.