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
4851996
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
4752017
Handbook of practical logic and automated reasoning
J Harrison
Cambridge University Press, 2009
4712009
Theorem proving with the real numbers
J Harrison
Springer Science & Business Media, 2012
3342012
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
3071992
HOL light: An overview
J Harrison
International Conference on Theorem Proving in Higher Order Logics, 60-66, 2009
2962009
The library of Isaac Newton.
J Harrison
The library of Isaac Newton, 1978
2501978
A machine-checked theory of floating point arithmetic
J Harrison
International Conference on Theorem Proving in Higher Order Logics, 113-130, 1999
1931999
Metatheory and reflection in theorem proving: A survey and critique
J Harrison
Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK, 1995
1781995
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
1771992
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
1692011
A skeptic's approach to combining HOL and Maple
J Harrison, L Théry
Journal of Automated Reasoning 21, 279-294, 1998
1611998
Formal proof—theory and practice
J Harrison
Notices of the AMS 55 (11), 1395-1406, 2008
1512008
The HOL Light theory of Euclidean space
J Harrison
Journal of Automated Reasoning 50, 173-190, 2013
1412013
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
1402000
History of interactive theorem proving
J Harrison, J Urban, F Wiedijk
Handbook of the History of Logic 9, 135-214, 2014
1262014
Towards self-verification of HOL Light
J Harrison
International Joint Conference on Automated Reasoning, 177-191, 2006
1232006
Floating point verification in HOL light: the exponential function
J Harrison
International Conference on Algebraic Methodology and Software Technology …, 1997
1191997
Formally verified mathematics
J Avigad, J Harrison
Communications of the ACM 57 (4), 66-75, 2014
1182014
The system can't perform the operation now. Try again later.
Articles 1–20