John Harrison: Complete publications list

This list is in reverse chronological order.

• 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. 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.
• 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. 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.
• 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 the Itanium(TM) Processor 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.
• 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.
• 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.