**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.

**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 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.

**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.

**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.

**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.

**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.

**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.