John Harrison: Complete publications list
This list is in reverse chronological order.

Formal proofs of hypergeometric sums.
(Dedicated to the memory of Andrzej Trybulec.)
Journal of Automated Reasoning, vol. 55, pp. 223243, 2015.

A Formal Proof of the Kepler Conjecture.
(With
Tom Hales and many others.)
ArXiV 1501.02155, 2015.

History of Interactive Theorem Proving.
(With Josef Urban and
Freek Wiedijk.)
Handbook of the History of Logic, vol. 9: Computational Logic,
pp. 135214, 2014.

Formally Verified Mathematics.
(With Jeremy Avigad.)
Communications of the ACM, vol. 57, no. 4, pp. 6675, 2014.

The HOL Light theory of Euclidean space.
Journal of Automated Reasoning, vol. 50, pp. 173190, 2013.

Some new results on decidability for elementary algebra and geometry.
(With Robert M. Solovay and
R.D.
Arthan.)
Annals of Pure and Applied Logic, vol. 163, pp. 17651802, 2012.

A formal proof of Pick's theorem.
Mathematical Structures in Computer Science, vol. 21, pp. 715729, 2011.
 Efficient and
accurate computation of upper bounds of approximation errors.
(With Sylvain
Chevillard,
Miorara Joldes and
Christoph Lauter.)
Theoretical Computer Science vol. 412, pp. 15231543, 2011.

Formal Verification. (Lecture notes from Marktoberdorf 2010.)

A formal proof of Pick's theorem (extended abstract).
Proceedings of ICMS 2010, Springer LNCS 6327, pp. 152154, 2010.
(This is superseded by the corresponding full paper)

A formalized proof of Dirichlet's theorem on primes in arithmetic
progression.
Journal of Formalized Reasoning, vol. 2, no. 1, pp. 6383, 2009.

Formalizing an analytic proof of the Prime Number Theorem.
Journal of Automated Reasoning, vol. 43, pp. 243261, 2009.

Without Loss of Generality.
Proceedings of TPHOLs 2009, Springer LNCS 5674, pp. 4359.

HOL Light: An Overview.
Proceedings of TPHOLs 2009, Springer LNCS 5674, pp. 6066.

Decimal Transcendentals via Binary.
Proceedings of ARITH19, IEEE Computer Society Press, 2009, pp. 187194.

Fast and Accurate Bessel Function Computation.
Proceedings of ARITH19, IEEE Computer Society Press, 2009, pp. 104113.
 I coedited the proceedings of
ARITH19, published by the IEEE
Computer Society Press, 2009.

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.
(This is superseded by the corresponding published paper)

A Revision of the Proof of the Kepler Conjecture.
(With Thomas C. Hales,
Sean McLaughlin,
Tobias Nipkow,
Steven Obua and
Roland
Zumkeller.)
Discrete and Computational Geometry, vol. 44, pp. 134, 2010
(first published online on 17th March 2009).

Handbook of Practical Logic and Automated Reasoning (book),
Cambridge University Press 2009.

A Software Implementation of the IEEE 754R Decimal FloatingPoint
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. 148162, 2009.

Formal Proof  Theory and Practice.
Notices of the American Mathematical Society, vol. 55, pp. 13951406,
2008.

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.
(This is superseded by the corresponding full paper)

Verifying nonlinear real formulas via sums of squares.
Proceedings of TPHOLs 2007, Springer LNCS vol. 4732, pp. 102118, 2007.

Automating elementary numbertheoretic proofs using Gröbner
bases.
Proceedings of CADE 21, Springer LNCS vol. 4603, pp. 5166, 2007.

A short survey of automated reasoning.
Proceedings of AB 2007, Springer LNCS vol. 4545, pp. 334349, 2007.

An Implementation of the IEEE 754R Decimal FloatingPoint Arithmetic
Using the Binary Encoding Format.
(With Marius Cornea, Cristina Anderson, Ping Tak Peter Tang, Eric
Schneider and Charles Tsen.)
Proceedings of the 18th IEEE Symposium on Computer Arithmetic, Montpellier,
France 2007, IEEE Computer Society Press, pp. 2937, 2007.

Formalizing basic complex analysis.
Festschrift in Honour of Andrzej Trybulec, Studies in Logic,
Grammar and Rhetoric vol. 10(23), pp. 151165, 2007.

Towards selfverification of HOL Light.
Proceedings of IJCAR 2006, the third International Joint Conference on
Automated Reasoning. Springer LNCS 4130, pp. 177191, 2006.
 I coedited the proceedings of
CSR 2006
(published as
LNCS 3967).

FloatingPoint 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. 211242, 2006.

A HOL Theory of Euclidean space.
Proceedings of TPHOLs 2005: 18th International Conference on
Theorem Proving in Higher Order Logics. Springer LNCS 3603, pp. 114129,
2005.

A ProofProducing Decision Procedure for Real Arithmetic.
(With Sean McLaughlin.)
Proceedings of CADE20: 20th International Conference on Automated
Deduction. Springer LNCS 3632, pp. 295314, 2005.

FloatingPoint Verification.
Proceedings of FM 2005: International Symposium of Formal Methods Europe
(Industry Day). Springer LNCS 3582, pp. 529532, 2005.
Also appears in special issues of
Computer Science of India
Communications (vol. 31 issue 2, pp. 1922) and
Journal of Universal Computer
Science (vol. 13 issue 5, pp. 629638).

Isolating critical cases for reciprocals using integer factorization.
Proceedings of the 16th IEEE Symposium on Computer Arithmetic, Santiago
de Compostela, Spain 2003, IEEE Computer Society Press, pp. 148157 2003.

Formal verification of square root algorithms
Formal Methods in System Design, vol. 22, pp. 143153, 2003.

Scientific Computing on Itaniumbased Systems (book,
with Marius Cornea and Ping Tak Peter Tang).
Intel Press, 2002.

Scientific Computing on the Itanium(TM) Processor.
(With Bruce Greer, Greg Henry, Wei Li and Peter Tang.)
Proceedings of Supercomputing conference, 2001.

Complex quantifier elimination in HOL.
Supplementary proceedings of the 2001 International Conference on
Theorem Proving in Higher Order Logics, pp. 159174, 2001.

Formal verification of floating point trigonometric functions.
Proceedings of the 3rd International Conference on Formal Methods in
ComputerAided Design, FMCAD 2000. Springer LNCS 1954, pp. 217233, 2000.

Formal verification of IA64 division algorithms.
Proceedings of the 13th International Conference on Theorem Proving in
Higher Order Logics, TPHOLs 2000. Springer LNCS 1869, pp. 234251, 2000.
 I coedited the proceedings of
TPHOLs 2000 (published as
LNCS 1869) as well as the supplemental proceedings
(OGI
technical report CSE 00009).

The Computation of Transcendental Functions on the IA64 Architecture.
(With Ted Kubaska, Shane Story and Peter Tang.)
Intel
Technology Journal, Q4 1999.

A MachineChecked Theory of Floating Point Arithmetic.
Appears in TPHOLs'99,
Springer LNCS 1690, pp. 113130, 1999.

Theorem Proving with the Real Numbers (book).
SpringerVerlag 1998.

Formalizing Dijkstra. Appears in
TPHOLs'98,
Springer LNCS 1497, pp. 171188, 1998.

Formalizing Basic First Order Model Theory. Appears in
TPHOLs'98,
Springer LNCS 1497, pp. 153170, 1998.

A Sceptic's Approach to Combining HOL and Maple.
(With
Laurent Théry.)
Journal of
Automated Reasoning, vol. 21, pp. 279294, 1998.

First Order Logic in Practice. Appears in
FTP'97.

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. 137152.
 Introduction
to Functional Programming. (Undergraduate lecture course.)

Proof Style. BRA Types workshop 1996, Springer LNCS 1512, pp. 154172.
Older version available as
Technical
Report number 410, University
of Cambridge Computer Laboratory,
January 1997.
 Theorem
proving with the real numbers (my PhD thesis). Technical
Report number 408, University
of Cambridge Computer Laboratory, December 1996.

HOL Light: A Tutorial Introduction.
Proceedings of the First International Conference on Formal Methods in
ComputerAided Design (FMCAD'96), Springer LNCS 1166, pp. 265269, 1996.

Formalized Mathematics
TUCS Technical
Report number 36, August 1996.

Pure Mathematics in a Mechanized Logic
Proceedings of the Finnish Artificial Intelligence Society
(FAIS) symposium: Logic, Mathematics and the Computer,
pp. 153169, 1996.
 I coedited the proceedings of TPHOLs'96
(published as LNCS
1125) as well as the supplementary
proceedings.

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. 221234, 1996.

A Mizar Mode for HOL
Proceedings of the 9th International Conference on Theorem Proving in
Higher Order Logics,
TPHOLs'96,
Springer LNCS 1125, pp. 203220, 1996.

Finding proofs and checking proofs
ECAI96 Workshop on
representation of mathematical knowledge.

Optimizing Proof Search in Model Elimination
Proceedings of the 13th International Conference on Automated Deduction
(CADE'13), Springer LNCS 1104, pp. 313327, 1996.
Longer version available as
TUCS
Technical Report number 6.

Formalized Mathematics
Unpublished draft, 22nd February 1996.

HOL Done Right
Unpublished draft, 21st August 1995.

Inductive definitions: automation and application
Proceedings of the 1995 International Workshop on Higher Order Logic
theorem proving and its applications, Aspen Grove, Utah, 1995.
Springer LNCS 971, pp. 200213, 1995.

Floating point verification in HOL.
Proceedings of the 1995 International Workshop on Higher Order Logic
theorem proving and its applications, Aspen Grove, Utah, 1995.
Springer LNCS 971, pp. 186199, 1995.

Reflections on Formalized Mathematics
Unpublished draft, 23rd August 1995.

Reflection; Practical Necessity or Not?
Summary of presentation at QED Workshop, Hotel Parkowa, Warsaw, 1995.

Binary Decision Diagrams as a HOL Derived Rule.
The Computer Journal, vol. 38, pp. 162170, 1995.

Metatheory and Reflection in Theorem Proving:
A Survey and Critique.
Technical Report CRC053,
SRI International Cambridge Computer Science Research Centre, 1995.

A Reference Version of HOL (with
Konrad Slind). Poster session of 1994 HOL Users Meeting;
only published in supplementary proceedings.

Binary decision diagrams as a HOL Derived Rule.
Proceedings of the 1994 International Workshop on Higher Order Logic
theorem proving and its applications, Valletta, Malta.
Springer LNCS 859, pp. 254268, 1994.

Constructing the Real Numbers in HOL.
Formal Methods in System Design, vol. 5, pp. 3559, 1994.

Extending the HOL Theorem Prover with a Computer Algebra System
to Reason about the Reals (with
Laurent Théry). Proceedings of the
1993 International Workshop on the HOL theorem proving system and its
applications, Vancouver. Springer LNCS 780, pp. 174184, 1993.

A HOL decision procedure for elementary real algebra.
Proceedings of the
1993 International Workshop on the HOL theorem proving system and its
applications, Vancouver. Springer LNCS 780, pp. 426436, 1993.

Reasoning about the reals: the marriage of HOL and Maple (with
Laurent Théry).
Proceedings of the 4th international conference on Logic Programming and
Automated Reasoning, Hotel Olgino, St. Petersburg. Springer LNCS 698,
pp. 351353, 1993.

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.
NorthHolland, IFIP Transactions A10, pp. 129156, 1993.

Constructing the real numbers in HOL.
Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher
Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium.
Volume A20 of IFIP Transactions A: Computer Science and Technology,
NorthHolland, pp. 145164, 1992.

The HOL reals Library.
Unpublished manual, 21st July 1992. Included in Cambridge HOL system's
standard release.

The HOL wellorder Library.
Unpublished manual, 30th May 1992. Included in Cambridge HOL system's
standard release.

The HOL reduce Library.
Unpublished manual, 18th May 1991. Included in Cambridge HOL system's
standard release.

Z88 Developers' Notes (with
Matthew Elton).
Cambridge Computer Ltd, 1988.