| 2025 | CAV | Relational Hoare Logic for Realistically Modelled Machine Code. | Denis Mazzucato, Abdalrhman Mohamed, Juneyoung Lee, Clark W. Barrett, Jim Grundy, John Harrison, Corina S. Pasareanu |
| 2016 | AVI | Engineering Study of Tidal Stream Renewable Energy Generation and Visualization: Issues of Process Modelling and Implementation. | John Harrison, James Uhomoibhi |
| 2011 | CRITIS | The Contribution of NEISAS to EP3R. | David Sutton, John Harrison, Sandro Bologna, Vittorio Rosato |
| 2011 | POPL | Robin Milner 1934--2010: verification, languages, and concurrency. | Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell |
| 2010 | SIGCSE | A k-12 college partnership. | Stephen Cooper, Wanda P. Dann, John Harrison |
| 2009 | ARITH | Fast and Accurate Bessel Function Computation. | John Harrison |
| 2009 | ARITH | Decimal Transcendentals via Binary. | John Harrison |
| 2008 | CAV | Theorem Proving for Verification (Invited Tutorial). | John Harrison |
| 2007 | ARITH | A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format. | Marius Cornea, Cristina Anderson, John Harrison, Ping Tak Peter Tang, Eric Schneider, Charles Tsen |
| 2007 | CADE | Automating Elementary Number-Theoretic Proofs Using Grbner Bases. | John Harrison |
| 2006 | CADE | Towards Self-verification of HOL Light. | John Harrison |
| 2005 | CADE | A Proof-Producing Decision Procedure for Real Arithmetic. | Sean McLaughlin, John Harrison |
| 2005 | FM | Floating-Point Verification. | John Harrison |
| 2003 | ARITH | Isolating Critical Cases for Reciprocals Using Integer Factorization. | John Harrison |
| 2003 | LICS | Formal Verification at Intel. | John Harrison |
| 2003 | WCAE | Intel Itanium floating-point architecture. | Marius Cornea, John Harrison, Ping Tak Peter Tang |
| 2002 | ICFEM | Enabling Hardware Verification through Design Changes. | Amr Talaat Abdel-Hamid, Sofine Tahar, John Harrison |
| 2001 | SC | Scientific computing on the Itanium processor. | Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Ping Tak Peter Tang |
| 2000 | CADE | High-Level Verification Using Theorem Proving and Formalized Mathematics. | John Harrison |
| 2000 | FMCAD | Formal Verification of Floating Point Trigonometric Functions. | John Harrison |
| 1996 | CADE | Optimizing Proof Search in Model Elimination. | John Harrison |
| 1996 | FMCAD | HOL Light: A Tutorial Introduction. | John Harrison |
| 1993 | LPAR | Reasoning About the Reals: The Marriage of HOL and Maple. | John Harrison, Laurent Thry |