Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDJohn Harrison 0001
Person information
- affiliation: Amazon Web Services, Portland, OR, USA
- affiliation (former): Intel Corporation, Hillsboro, OR, USA
- affiliation (PhD 1996): University of Cambridge, UK
- affiliation (former): Åbo Akademi University, Turku, Finland
Other persons with the same name
- John Harrison — disambiguation page
- John Harrison 0002 — University of Liverpool, Department of Psychological Sciences, UK
- John Harrison 0003 — University of Queensland, School of Journalism and Communication, Brisbane, QLD, Australia
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2009
[b2]John Harrison:
Handbook of Practical Logic and Automated Reasoning. Cambridge University Press 2009, ISBN 978-0-521-89957-4, pp. I-XIX, 1-681- 1998
- [b1]John Harrison:
Theorem proving with the real numbers. University of Cambridge, UK, CPHC/BCS distinguished dissertations, Springer 1998, ISBN 978-3-540-76256-0, pp. I-XII, 1-186
Journal Articles
- 2018
- [j19]Warren E. Ferguson
, Jesse Bingham, Levent Erkök, John R. Harrison, Joe Leslie-Hurd:
Digit Serial Methods with Applications to Division and Square Root. IEEE Trans. Computers 67(3): 449-456 (2018) - 2016
- [j18]John Harrison, Josef Urban, Freek Wiedijk:
Preface: Twenty Years of the QED Manifesto. J. Formaliz. Reason. 9(1): 1-2 (2016) - 2015
- [j17]John Harrison:
Formal Proofs of Hypergeometric Sums - Dedicated to the memory of Andrzej Trybulec. J. Autom. Reason. 55(3): 223-243 (2015) - 2014
- [j16]Jeremy Avigad, John Harrison:
Formally verified mathematics. Commun. ACM 57(4): 66-75 (2014) - 2013
- [j15]John Harrison:
The HOL Light Theory of Euclidean Space. J. Autom. Reason. 50(2): 173-190 (2013) - 2012
- [j14]Robert Solovay, R. D. Arthan, John Harrison:
Some new results on decidability for elementary algebra and geometry. Ann. Pure Appl. Log. 163(12): 1765-1802 (2012) - 2011
- [j13]John Harrison:
A formal proof of Pick's Theorem. Math. Struct. Comput. Sci. 21(4): 715-729 (2011) - 2010
- [j12]Behzad Akbarpour, Amr Talaat Abdel-Hamid, Sofiène Tahar, John Harrison:
Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. Comput. J. 53(4): 465-488 (2010) - [j11]Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller:
A Revision of the Proof of the Kepler Conjecture. Discret. Comput. Geom. 44(1): 1-34 (2010) - 2009
- [j10]John Harrison:
Formalizing an Analytic Proof of the Prime Number Theorem. J. Autom. Reason. 43(3): 243-261 (2009) - [j9]John Harrison:
A formalized proof of Dirichlet's theorem on primes in arithmetic progression. J. Formaliz. Reason. 2(1): 63-83 (2009) - [j8]Marius Cornea, John Harrison, Cristina Anderson, Ping Tak Peter Tang, Eric Schneider, Evgeny Gvozdev:
A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format. IEEE Trans. Computers 58(2): 148-162 (2009) - 2007
- [j7]John Harrison:
Floating-Point Verification. J. Univers. Comput. Sci. 13(5): 629-638 (2007) - 2003
- [j6]John Harrison:
Formal Verification of Square Root Algorithms. Formal Methods Syst. Des. 22(2): 143-153 (2003) - 2002
- [j5]Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Ping Tak Peter Tang:
Scientific computing on the Itanium® processor. Sci. Program. 10(4): 329-337 (2002) - 2000
- [j4]John Harrison:
Floating Point Verification in HOL Light: The Exponential Function. Formal Methods Syst. Des. 16(3): 271-305 (2000) - 1998
- [j3]John Harrison, Laurent Théry:
A Skeptic's Approach to Combining HOL and Maple. J. Autom. Reason. 21(3): 279-294 (1998) - 1995
- [j2]John Harrison:
Binary Decision Diagrams as a HOL Derived Rule. Comput. J. 38(2): 162-170 (1995) - 1994
- [j1]John Harrison:
Constructing the Real Numbers in HOL. Formal Methods Syst. Des. 5(1/2): 35-59 (1994)
Conference and Workshop Papers
- 2011
- [c42]Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell:
Robin Milner 1934--2010: verification, languages, and concurrency. POPL 2011: 473-474 - 2010
- [c41]John Harrison:
A Formal Proof of Pick's Theorem - (Extended Abstract). ICMS 2010: 152-154 - 2009
- [c40]John Harrison:
Fast and Accurate Bessel Function Computation. IEEE Symposium on Computer Arithmetic 2009: 104-113 - [c39]John Harrison:
Decimal Transcendentals via Binary. IEEE Symposium on Computer Arithmetic 2009: 187-194 - [c38]John Harrison:
Without Loss of Generality. TPHOLs 2009: 43-59 - [c37]John Harrison:
HOL Light: An Overview. TPHOLs 2009: 60-66 - 2008
- [c36]John Harrison:
Theorem Proving for Verification (Invited Tutorial). CAV 2008: 11-18 - 2007
- [c35]John Harrison:
A Short Survey of Automated Reasoning. AB 2007: 334-349 - [c34]Marius Cornea, Cristina Anderson, John Harrison, Ping Tak Peter Tang, Eric Schneider, Charles Tsen:
A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format. IEEE Symposium on Computer Arithmetic 2007: 29-37 - [c33]John Harrison:
Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. CADE 2007: 51-66 - [c32]John Harrison:
Verifying Nonlinear Real Formulas Via Sums of Squares. TPHOLs 2007: 102-118 - 2006
- [c31]John Harrison:
Towards Self-verification of HOL Light. IJCAR 2006: 177-191 - [c30]John Harrison:
Floating-Point Verification Using Theorem Proving. SFM 2006: 211-242 - 2005
- [c29]Sean McLaughlin, John Harrison:
A Proof-Producing Decision Procedure for Real Arithmetic. CADE 2005: 295-314 - [c28]John Harrison:
Floating-Point Verification. FM 2005: 529-532 - [c27]John Harrison:
A HOL Theory of Euclidean Space. TPHOLs 2005: 114-129 - 2003
- [c26]John Harrison:
Isolating Critical Cases for Reciprocals Using Integer Factorization. IEEE Symposium on Computer Arithmetic 2003: 148-157 - [c25]John Harrison:
Formal Verification at Intel. LICS 2003: 45- - [c24]Marius Cornea, John Harrison, Ping Tak Peter Tang:
Intel® Itanium® floating-point architecture. WCAE 2003: 3 - 2002
- [c23]Amr Talaat Abdel-Hamid, Sofiène Tahar, John Harrison:
Enabling Hardware Verification through Design Changes. ICFEM 2002: 459-470 - 2001
- [c22]Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Ping Tak Peter Tang:
Scientific computing on the Itanium processor. SC 2001: 41 - 2000
- [c21]John Harrison:
High-Level Verification Using Theorem Proving and Formalized Mathematics. CADE 2000: 1-6 - [c20]John Harrison:
Formal Verification of Floating Point Trigonometric Functions. FMCAD 2000: 217-233 - [c19]John Harrison:
Formal Verification of IA-64 Division Algorithms. TPHOLs 2000: 233-251 - 1999
- [c18]John Harrison:
A Machine-Checked Theory of Floating Point Arithmetic. TPHOLs 1999: 113-130 - 1998
- [c17]John Harrison:
Formalizing Basic First Order Model Theory. TPHOLs 1998: 153-170 - [c16]John Harrison:
Formalizing Dijkstra. TPHOLs 1998: 171-188 - 1997
- [c15]John Harrison:
Floating Point Verification in HOL Light: The Exponential Function. AMAST 1997: 246-260 - [c14]John Harrison:
Verifying the Accuracy of Polynomial Approximations in HOL. TPHOLs 1997: 137-152 - 1996
- [c13]John Harrison:
Optimizing Proof Search in Model Elimination. CADE 1996: 313-327 - [c12]John Harrison:
HOL Light: A Tutorial Introduction. FMCAD 1996: 265-269 - [c11]John Harrison:
A Mizar Mode for HOL. TPHOLs 1996: 203-220 - [c10]John Harrison:
Stålmarck's Algorithm as a HOL Derived Rule. TPHOLs 1996: 221-234 - [c9]John Harrison:
Proof Style. TYPES 1996: 154-172 - 1995
- [c8]John Harrison:
Floating Point Verification in HOL. TPHOLs 1995: 186-199 - [c7]John Harrison:
Inductive Definitions: Automation and Application. TPHOLs 1995: 200-213 - 1994
- [c6]John Harrison:
Binary Decision Diagrams as a HOL Derived Rule. TPHOLs 1994: 254-268 - 1993
- [c5]John Harrison, Laurent Théry:
Reasoning About the Reals: The Marriage of HOL and Maple. LPAR 1993: 351-353 - [c4]John Harrison, Laurent Théry:
Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. HUG 1993: 174-184 - [c3]John Harrison:
A HOL Decision Procedure for Elementary Real Algebra. HUG 1993: 426-435 - 1992
- [c2]Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel:
Experience with Embedding Hardware Description Languages in HOL. TPCD 1992: 129-156 - [c1]John Harrison:
Constructing the real numbers in HOL. TPHOLs 1992: 145-164
Parts in Books or Collections
- 2011
- [p2]John Harrison:
Formal Verification. Software and Systems Safety - Specification and Verification 2011: 103-157 - 2006
- [p1]John Harrison, Konrad Slind, Rob Arthan:
HOL. The Seventeen Provers of the World 2006: 11-19
Editorship
- 2019
- [e5]John Harrison, John O'Leary, Andrew Tolmach:
10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA. LIPIcs 141, Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2019, ISBN 978-3-95977-122-1 [contents] - 2009
- [e4]Javier D. Bruguera, Marius Cornea, Debjit Das Sarma, John Harrison:
19th IEEE Symposium on Computer Arithmetic, ARITH 2009, Portland, Oregon, USA, 9-10 June 2009. IEEE Computer Society 2009, ISBN 978-0-7695-3670-5 [contents] - 2006
- [e3]Dima Grigoriev, John Harrison, Edward A. Hirsch:
Computer Science - Theory and Applications, First International Symposium on Computer Science in Russia, CSR 2006, St. Petersburg, Russia, June 8-12, 2006, Proceedings. Lecture Notes in Computer Science 3967, Springer 2006, ISBN 3-540-34166-8 [contents] - 2000
- [e2]Mark D. Aagaard, John Harrison:
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings. Lecture Notes in Computer Science 1869, Springer 2000, ISBN 3-540-67863-8 [contents] - 1996
- [e1]Joakim von Wright, Jim Grundy, John Harrison:
Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings. Lecture Notes in Computer Science 1125, Springer 1996, ISBN 3-540-61587-3 [contents]
Reference Works
- 2014
- [r1]John Harrison, Josef Urban, Freek Wiedijk:
History of Interactive Theorem Proving. Computational Logic 2014: 135-214
Informal and Other Publications
- 2017
- [i3]Warren E. Ferguson, Jesse Bingham, Levent Erkök, John R. Harrison, Joe Leslie-Hurd:
Digit Serial Methods with Applications to Division and Square Root (with mechanically checked correctness proofs). CoRR abs/1708.00140 (2017) - 2015
- [i2]Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller:
A formal proof of the Kepler conjecture. CoRR abs/1501.02155 (2015) - 2006
- [i1]Christoph Benzmüller, John Harrison, Carsten Schürmann:
LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL). CoRR abs/cs/0601042 (2006)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-03 21:17 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
