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
4451996
Handbook of practical logic and automated reasoning
J Harrison
Cambridge University Press, 2009
4242009
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
3432017
Theorem proving with the real numbers
J Harrison
Springer Science & Business Media, 2012
3322012
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
2861992
HOL light: An overview
J Harrison
International Conference on Theorem Proving in Higher Order Logics, 60-66, 2009
2512009
The library of Isaac Newton.
J Harrison
The library of Isaac Newton, 1978
2201978
A machine-checked theory of floating point arithmetic
J Harrison
International Conference on Theorem Proving in Higher Order Logics, 113-130, 1999
1761999
Metatheory and reflection in theorem proving: A survey and critique
J Harrison
Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995
1741995
A skeptic's approach to combining HOL and Maple
J Harrison, L Théry
Journal of Automated Reasoning 21 (3), 279-294, 1998
1551998
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
1542011
A HOL theory of Euclidean space
J Harrison
International conference on theorem proving in higher order logics, 114-129, 2005
1382005
Formal verification of floating point trigonometric functions
J Harrison
International conference on formal methods in computer-aided design, 254-270, 2000
1352000
The HOL Light theory of Euclidean space
J Harrison
Journal of Automated Reasoning 50 (2), 173-190, 2013
1332013
Formal proof—theory and practice
J Harrison
Notices of the AMS 55 (11), 1395-1406, 2008
1302008
Towards self-verification of HOL Light
J Harrison
International Joint Conference on Automated Reasoning, 177-191, 2006
1152006
Floating point verification in HOL light: the exponential function
J Harrison
International Conference on Algebraic Methodology and Software Technology …, 1997
1151997
Scientific computing on Itanium-based systems
M Cornea, J Harrison, PTP Tang
Intel press, 2002
1082002
Verifying nonlinear real formulas via sums of squares
J Harrison
International Conference on Theorem Proving in Higher Order Logics, 102-118, 2007
1042007
A Mizar mode for HOL
J Harrison
International Conference on Theorem Proving in Higher Order Logics, 203-220, 1996
1031996
The system can't perform the operation now. Try again later.
Articles 1–20