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

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, e2, 2017 | 475 | 2017 |

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

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

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

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

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

Metatheory and reflection in theorem proving: A survey and critique J Harrison Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995 | 178 | 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 | 177 | 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 | 169 | 2011 |

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

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

The HOL Light theory of Euclidean space J Harrison Journal of Automated Reasoning 50, 173-190, 2013 | 141 | 2013 |

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

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

History of interactive theorem proving J Harrison, J Urban, F Wiedijk Handbook of the History of Logic 9, 135-214, 2014 | 126 | 2014 |

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

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

Formally verified mathematics J Avigad, J Harrison Communications of the ACM 57 (4), 66-75, 2014 | 118 | 2014 |