John Harrison

Orcid: 0000-0001-5707-4631

Affiliations:

Amazon Web Services, Portland, OR, USA
Intel Corporation, Hillsboro, OR, USA (former)
University of Cambridge, UK (PhD 1996)
Åbo Akademi University, Turku, Finland (former)

According to our database¹, John Harrison authored at least 65 papers between 1992 and 2018.

Collaborative distances:

Dijkstra number² of three.
Erdős number³ of three.

Timeline

Legend:

Book

In proceedings

Article

PhD thesis

Dataset

Other

Bibliography

2018

Digit Serial Methods with Applications to Division and Square Root.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2018

2017

Digit Serial Methods with Applications to Division and Square Root (with mechanically checked correctness proofs).

[BibT_eX]

[DOI]

CoRR, 2017

2016

Preface: Twenty Years of the QED Manifesto.

[BibT_eX]

[DOI]

John Harrison

Josef Urban

Freek Wiedijk

J. Formaliz. Reason., 2016

2015

Formal Proofs of Hypergeometric Sums - Dedicated to the memory of Andrzej Trybulec.

[BibT_eX]

[DOI]

John Harrison

J. Autom. Reason., 2015

A formal proof of the Kepler conjecture.

[BibT_eX]

[DOI]

CoRR, 2015

2014

History of Interactive Theorem Proving.

[BibT_eX]

[DOI]

John Harrison

Josef Urban

Freek Wiedijk

Proceedings of the Computational Logic, 2014

Formally verified mathematics.

[BibT_eX]

[DOI]

Jeremy Avigad

John Harrison

Commun. ACM, 2014

2013

The HOL Light Theory of Euclidean Space.

[BibT_eX]

[DOI]

John Harrison

J. Autom. Reason., 2013

2012

Some new results on decidability for elementary algebra and geometry.

[BibT_eX]

[DOI]

Robert Solovay

R. D. Arthan

John Harrison

Ann. Pure Appl. Log., 2012

2011

Formal Verification.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Software and Systems Safety - Specification and Verification, 2011

A formal proof of Pick's Theorem.

[BibT_eX]

[DOI]

John Harrison

Math. Struct. Comput. Sci., 2011

Robin Milner 1934--2010: verification, languages, and concurrency.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

2010

A Revision of the Proof of the Kepler Conjecture.

[BibT_eX]

[DOI]

Discret. Comput. Geom., 2010

Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL.

[BibT_eX]

[DOI]

Behzad Akbarpour

Amr Talaat Abdel-Hamid

Sofiène Tahar

John Harrison

Comput. J., 2010

A Formal Proof of Pick's Theorem - (Extended Abstract).

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Mathematical Software, 2010

2009

A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 2009

A formalized proof of Dirichlet's theorem on primes in arithmetic progression.

[BibT_eX]

[DOI]

John Harrison

J. Formaliz. Reason., 2009

Formalizing an Analytic Proof of the Prime Number Theorem.

[BibT_eX]

[DOI]

John Harrison

J. Autom. Reason., 2009

HOL Light: An Overview.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Without Loss of Generality.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Decimal Transcendentals via Binary.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the 19th IEEE Symposium on Computer Arithmetic, 2009

Fast and Accurate Bessel Function Computation.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the 19th IEEE Symposium on Computer Arithmetic, 2009

Handbook of Practical Logic and Automated Reasoning.

[BibT_eX]

John Harrison

Cambridge University Press, ISBN: 978-0-521-89957-4, 2009

2008

Theorem Proving for Verification (Invited Tutorial).

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Floating-Point Verification.

[BibT_eX]

[DOI]

John Harrison

J. Univers. Comput. Sci., 2007

Verifying Nonlinear Real Formulas Via Sums of Squares.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Automating Elementary Number-Theoretic Proofs Using Gröbner Bases.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Automated Deduction, 2007

A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Computer Arithmetic (ARITH-18 2007), 2007

A Short Survey of Automated Reasoning.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Algebraic Biology, Second International Conference, 2007

2006

LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)

[BibT_eX]

[DOI]

Christoph Benzmüller

John Harrison

Carsten Schürmann

CoRR, 2006

HOL.

[BibT_eX]

[DOI]

John Harrison

Konrad Slind

Rob Arthan

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

Floating-Point Verification Using Theorem Proving.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Formal Methods for Hardware Verification, 2006

Towards Self-verification of HOL Light.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005

A HOL Theory of Euclidean Space.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

A Proof-Producing Decision Procedure for Real Arithmetic.

[BibT_eX]

[DOI]

Sean McLaughlin

John Harrison

Proceedings of the Automated Deduction, 2005

2003

Formal Verification of Square Root Algorithms.

[BibT_eX]

[DOI]

John Harrison

Formal Methods Syst. Des., 2003

Intel® Itanium® floating-point architecture.

[BibT_eX]

[DOI]

Marius Cornea

John Harrison

Ping Tak Peter Tang

Proceedings of the 2003 workshop on Computer architecture education, 2003

Formal Verification at Intel.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

Isolating Critical Cases for Reciprocals Using Integer Factorization.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the 16th IEEE Symposium on Computer Arithmetic (Arith-16 2003), 2003

2002

Scientific computing on the Itanium® processor.

[BibT_eX]

[DOI]

Sci. Program., 2002

Enabling Hardware Verification through Design Changes.

[BibT_eX]

[DOI]

Amr Talaat Abdel-Hamid

Sofiène Tahar

John Harrison

Proceedings of the Formal Methods and Software Engineering, 2002

2001

Scientific computing on the Itanium processor.

[BibT_eX]

[DOI]

Proceedings of the 2001 ACM/IEEE conference on Supercomputing, 2001

2000

Floating Point Verification in HOL Light: The Exponential Function.

[BibT_eX]

[DOI]

John Harrison

Formal Methods Syst. Des., 2000

Formal Verification of IA-64 Division Algorithms.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

Formal Verification of Floating Point Trigonometric Functions.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

High-Level Verification Using Theorem Proving and Formalized Mathematics.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Automated Deduction, 2000

1999

A Machine-Checked Theory of Floating Point Arithmetic.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 12th International Conference, 1999

1998

A Skeptic's Approach to Combining HOL and Maple.

[BibT_eX]

[DOI]

John Harrison

Laurent Théry

J. Autom. Reason., 1998

Formalizing Dijkstra.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

Formalizing Basic First Order Model Theory.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

Theorem proving with the real numbers.

[BibT_eX]

[DOI]

John Harrison

CPHC/BCS distinguished dissertations, Springer, ISBN: 978-3-540-76256-0, 1998

1997

Verifying the Accuracy of Polynomial Approximations in HOL.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997

1996

Proof Style.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Types for Proofs and Programs, 1996

Stålmarck's Algorithm as a HOL Derived Rule.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

A Mizar Mode for HOL.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

HOL Light: A Tutorial Introduction.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Optimizing Proof Search in Model Elimination.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995

Binary Decision Diagrams as a HOL Derived Rule.

[BibT_eX]

[DOI]

John Harrison

Comput. J., 1995

Inductive Definitions: Automation and Application.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Higher Order Logic Theorem Proving and Its Applications, 1995

Floating Point Verification in HOL.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Higher Order Logic Theorem Proving and Its Applications, 1995

1994

Constructing the Real Numbers in HOL.

[BibT_eX]

[DOI]

John Harrison

Formal Methods Syst. Des., 1994

1993

Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.

[BibT_eX]

[DOI]

John Harrison

Laurent Théry

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

A HOL Decision Procedure for Elementary Real Algebra.

[BibT_eX]

[DOI]

John Harrison

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Reasoning About the Reals: The Marriage of HOL and Maple.

[BibT_eX]

[DOI]

John Harrison

Laurent Théry

Proceedings of the Logic Programming and Automated Reasoning,4th International Conference, 1993

1992

Experience with Embedding Hardware Description Languages in HOL.

[BibT_eX]

Proceedings of the Theorem Provers in Circuit Design, 1992

John Harrison

Timeline

Legend:

Links

Online presence:

On csauthors.net:

Bibliography

Loading...