HOL Light: A tutorial introduction J Harrison International Conference on Formal Methods in Computer-Aided Design, 265-269, 1996 | 445 | 1996 |

Handbook of practical logic and automated reasoning J Harrison Cambridge University Press, 2009 | 424 | 2009 |

A formal proof of the Kepler conjecture T Hales, M Adams, G Bauer, TD Dang, J Harrison, H Le Truong, ... Forum of mathematics, Pi 5, 2017 | 343 | 2017 |

Theorem proving with the real numbers J Harrison Springer Science & Business Media, 2012 | 332 | 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 | 286 | 1992 |

HOL light: An overview J Harrison International Conference on Theorem Proving in Higher Order Logics, 60-66, 2009 | 251 | 2009 |

The library of Isaac Newton. J Harrison The library of Isaac Newton, 1978 | 220 | 1978 |

A machine-checked theory of floating point arithmetic J Harrison International Conference on Theorem Proving in Higher Order Logics, 113-130, 1999 | 176 | 1999 |

Metatheory and reflection in theorem proving: A survey and critique J Harrison Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995 | 174 | 1995 |

A skeptic's approach to combining HOL and Maple J Harrison, L Théry Journal of Automated Reasoning 21 (3), 279-294, 1998 | 155 | 1998 |

A revision of the proof of the Kepler conjecture TC Hales, J Harrison, S McLaughlin, T Nipkow, S Obua, R Zumkeller The Kepler Conjecture, 341-376, 2011 | 154 | 2011 |

A HOL theory of Euclidean space J Harrison International conference on theorem proving in higher order logics, 114-129, 2005 | 138 | 2005 |

Formal verification of floating point trigonometric functions J Harrison International conference on formal methods in computer-aided design, 254-270, 2000 | 135 | 2000 |

The HOL Light theory of Euclidean space J Harrison Journal of Automated Reasoning 50 (2), 173-190, 2013 | 133 | 2013 |

Formal proof—theory and practice J Harrison Notices of the AMS 55 (11), 1395-1406, 2008 | 130 | 2008 |

Towards self-verification of HOL Light J Harrison International Joint Conference on Automated Reasoning, 177-191, 2006 | 115 | 2006 |

Floating point verification in HOL light: the exponential function J Harrison International Conference on Algebraic Methodology and Software Technology …, 1997 | 115 | 1997 |

Scientific computing on Itanium-based systems M Cornea, J Harrison, PTP Tang Intel press, 2002 | 108 | 2002 |

Verifying nonlinear real formulas via sums of squares J Harrison International Conference on Theorem Proving in Higher Order Logics, 102-118, 2007 | 104 | 2007 |

A Mizar mode for HOL J Harrison International Conference on Theorem Proving in Higher Order Logics, 203-220, 1996 | 103 | 1996 |