Follow
John R Harrison
John R Harrison
Amazon Web Services
Verified email at amazon.com - Homepage
Title
Cited by
Cited by
Year
HOL Light: A tutorial introduction
J Harrison
International Conference on Formal Methods in Computer-Aided Design, 265-269, 1996
4741996
Handbook of practical logic and automated reasoning
J Harrison
Cambridge University Press, 2009
4572009
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
4252017
Theorem proving with the real numbers
J Harrison
Springer Science & Business Media, 2012
3372012
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
3021992
HOL light: An overview
J Harrison
International Conference on Theorem Proving in Higher Order Logics, 60-66, 2009
2872009
The library of Isaac Newton.
J Harrison
The library of Isaac Newton, 1978
2431978
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
2062011
A machine-checked theory of floating point arithmetic
J Harrison
International Conference on Theorem Proving in Higher Order Logics, 113-130, 1999
1871999
Metatheory and reflection in theorem proving: A survey and critique
J Harrison
Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995
1791995
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
1711992
A skeptic's approach to combining HOL and Maple
J Harrison, L Théry
Journal of Automated Reasoning 21, 279-294, 1998
1581998
Formal proof—theory and practice
J Harrison
Notices of the AMS 55 (11), 1395-1406, 2008
1422008
A HOL theory of Euclidean space
J Harrison
International conference on theorem proving in higher order logics, 114-129, 2005
1412005
Formal verification of floating point trigonometric functions
J Harrison
International conference on formal methods in computer-aided design, 254-270, 2000
1392000
The HOL Light theory of Euclidean space
J Harrison
Journal of Automated Reasoning 50, 173-190, 2013
1372013
Towards self-verification of HOL Light
J Harrison
International Joint Conference on Automated Reasoning, 177-191, 2006
1222006
Floating point verification in HOL light: the exponential function
J Harrison
International Conference on Algebraic Methodology and Software Technology …, 1997
1191997
Scientific computing on Itanium-based systems
M Cornea, J Harrison, PTP Tang
Intel press, 2002
1142002
Formally verified mathematics
J Avigad, J Harrison
Communications of the ACM 57 (4), 66-75, 2014
1122014
The system can't perform the operation now. Try again later.
Articles 1–20