| A formal proof of the Kepler conjecture T Hales, M Adams, G Bauer, TD Dang, J Harrison, LT Hoang, C Kaliszyk, ... Forum of mathematics, Pi 5, e2, 2017 | 555 | 2017 |
| Handbook of practical logic and automated reasoning J Harrison Cambridge University Press, 2009 | 518 | 2009 |
| HOL Light: A tutorial introduction J Harrison International Conference on Formal Methods in Computer-Aided Design, 265-269, 1996 | 517 | 1996 |
| HOL light: An overview J Harrison International Conference on Theorem Proving in Higher Order Logics, 60-66, 2009 | 350 | 2009 |
| Theorem proving with the real numbers J Harrison Springer Science & Business Media, 2012 | 349 | 2012 |
| Experience with embedding hardware description languages in HOL. RJ Boulton, AD Gordon, MJC Gordon, J Harrison, J Herbert, J Van Tassel TPCD 10, 129-156, 1992 | 322 | 1992 |
| The Library of Isaac Newton J Harrison Cambridge University Press 98, 119-20, 1978 | 260 | 1978 |
| A machine-checked theory of floating point arithmetic J Harrison International Conference on Theorem Proving in Higher Order Logics, 113-130, 1999 | 206 | 1999 |
| History of interactive theorem proving J Harrison, J Urban, F Wiedijk Handbook of the History of Logic 9, 135-214, 2014 | 180 | 2014 |
| Metatheory and reflection in theorem proving: A survey and critique J Harrison Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995 | 179 | 1995 |
| An investigation of the relationship between microbial and particulate indoor air pollution and the sick building syndrome J Harrison, CAC Pickering, EB Faragher, PKC Austwick, SA Little, ... Respiratory Medicine 86 (3), 225-235, 1992 | 178 | 1992 |
| A revision of the proof of the Kepler conjecture TC Hales, J Harrison, S McLaughlin, T Nipkow, S Obua, R Zumkeller The Kepler Conjecture: The Hales-Ferguson Proof, 341-376, 2011 | 177 | 2011 |
| A skeptic's approach to combining HOL and Maple J Harrison, L Théry Journal of Automated Reasoning 21 (3), 279-294, 1998 | 160 | 1998 |
| Formal proof—theory and practice J Harrison Notices of the AMS 55 (11), 1395-1406, 2008 | 157 | 2008 |
| The HOL Light theory of Euclidean space J Harrison Journal of Automated Reasoning 50 (2), 173-190, 2013 | 153 | 2013 |
| Formally verified mathematics J Avigad, J Harrison Communications of the ACM 57 (4), 66-75, 2014 | 146 | 2014 |
| A HOL theory of Euclidean space J Harrison International conference on theorem proving in higher order logics, 114-129, 2005 | 144 | 2005 |
| Formal verification of floating point trigonometric functions J Harrison International conference on formal methods in computer-aided design, 254-270, 2000 | 142 | 2000 |
| Floating point verification in HOL light: the exponential function J Harrison International Conference on Algebraic Methodology and Software Technology …, 1997 | 133 | 1997 |
| Towards self-verification of HOL Light J Harrison International Joint Conference on Automated Reasoning, 177-191, 2006 | 125 | 2006 |
