John Harrison: Complete publications list

• Formal proofs of hypergeometric sums. (Dedicated to the memory of Andrzej Trybulec.) Journal of Automated Reasoning, vol. 55, pp. 223-243, 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. 135-214, 2014.
• Formally Verified Mathematics. (With Jeremy Avigad.) Communications of the ACM, vol. 57, no. 4, pp. 66-75, 2014.
• The HOL Light theory of Euclidean space. Journal of Automated Reasoning, vol. 50, pp. 173-190, 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. 1765-1802, 2012.
• A formal proof of Pick's theorem. Mathematical Structures in Computer Science, vol. 21, pp. 715-729, 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. 1523-1543, 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. 152-154, 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. 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.
• HOL Light: An Overview. Proceedings of TPHOLs 2009, Springer LNCS 5674, pp. 60-66.
• 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.
• I co-edited the proceedings of ARITH-19, 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. 1-34, 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 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.
• Formal Proof -- Theory and Practice. Notices of the American Mathematical Society, vol. 55, pp. 1395-1406, 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. 102-118, 2007.
• Automating elementary number-theoretic proofs using Gröbner bases. Proceedings of CADE 21, Springer LNCS vol. 4603, pp. 51-66, 2007.
• A short survey of automated reasoning. Proceedings of AB 2007, Springer LNCS vol. 4545, pp. 334-349, 2007.
• An 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 Charles Tsen.) Proceedings of the 18th IEEE Symposium on Computer Arithmetic, Montpellier, France 2007, IEEE Computer Society Press, pp. 29-37, 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.
• I co-edited the proceedings of CSR 2006 (published as LNCS 3967).
• 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.
• 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. (With Sean McLaughlin.) Proceedings of CADE-20: 20th International Conference on Automated Deduction. Springer LNCS 3632, pp. 295-314, 2005.
• Floating-Point Verification. Proceedings of FM 2005: International Symposium of Formal Methods Europe (Industry Day). Springer LNCS 3582, pp. 529-532, 2005. Also appears in special issues of Computer Science of India Communications (vol. 31 issue 2, pp. 19-22) and Journal of Universal Computer Science (vol. 13 issue 5, pp. 629-638).
• 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. 148-157 2003.
• Formal verification of square root algorithms Formal Methods in System Design, vol. 22, pp. 143-153, 2003.
• Scientific Computing on Itanium-based 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. 159-174, 2001.
• 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.
• I co-edited the proceedings of TPHOLs 2000 (published as LNCS 1869) as well as the supplemental proceedings (OGI technical report CSE 00-009).
• The Computation of Transcendental Functions on the IA-64 Architecture. (With Ted Kubaska, Shane Story and Peter Tang.) Intel Technology Journal, Q4 1999.
• A Machine-Checked Theory of Floating Point Arithmetic. Appears in TPHOLs'99, Springer LNCS 1690, pp. 113-130, 1999.
• Theorem Proving with the Real Numbers (book). Springer-Verlag 1998.
• Formalizing Dijkstra. Appears in TPHOLs'98, Springer LNCS 1497, pp. 171-188, 1998.
• Formalizing Basic First Order Model Theory. Appears in TPHOLs'98, Springer LNCS 1497, pp. 153-170, 1998.
• 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 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. 137-152.
• Introduction to Functional Programming. (Undergraduate lecture course.)
• Proof Style. BRA Types workshop 1996, Springer LNCS 1512, pp. 154-172. 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 Computer-Aided Design (FMCAD'96), Springer LNCS 1166, pp. 265-269, 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. 153-169, 1996.
• I co-edited 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. 221-234, 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. 203-220, 1996.
• Finding proofs and checking proofs ECAI-96 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. 313-327, 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. 200-213, 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. 186-199, 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. 162-170, 1995.
• Metatheory and Reflection in Theorem Proving: A Survey and Critique. Technical Report CRC-053, 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. 254-268, 1994.
• Constructing the Real Numbers in HOL. Formal Methods in System Design, vol. 5, pp. 35-59, 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. 174-184, 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. 426-436, 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. 351-353, 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. North-Holland, IFIP Transactions A-10, pp. 129-156, 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 A-20 of IFIP Transactions A: Computer Science and Technology, North-Holland, pp. 145-164, 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.