# John Harrison

According to our database

Collaborative distances:

^{1}, John Harrison authored at least 78 papers between 1992 and 2016.Collaborative distances:

## Timeline

#### Legend:

Book In proceedings Article PhD thesis Other## Links

#### On csauthors.net:

## Bibliography

2016

Preface: Twenty Years of the QED Manifesto.

J. Formalized Reasoning, 2016

Engineering Study of Tidal Stream Renewable Energy Generation and Visualization: Issues of Process Modelling and Implementation.

Proceedings of the Advanced Visual Interfaces. Supporting Big Data Applications, 2016

2015

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

J. Autom. Reasoning, 2015

Questionable Benefit of Visual and Peer Mediated Learning on Overall Learning Outcomes of a First-Year Physiology Course.

IJMBL, 2015

2014

History of Interactive Theorem Proving.

Proceedings of the Computational Logic, 2014

Formally verified mathematics.

Commun. ACM, 2014

Integrating Data Mining and Data Management Technologies for Scholarly Inquiry.

Proceedings of the 2014 IEEE International Conference on Big Data, 2014

2013

The HOL Light Theory of Euclidean Space.

J. Autom. Reasoning, 2013

Anywhere, anytime, with any device: scenario-based mobile learning in biomedical sciences.

IJMLO, 2013

Evolving Persistent Archives and Digital Library Systems: Integrating iRods, Cheshire3 and Multivalent.

IJDC, 2013

2012

Re-envisioning instructional technology research in higher education environments: a content analysis of a grant program.

J. Computing in Higher Education, 2012

Mobile learning materials as a 'prompt' for participation in physiology practical classes.

IJMLO, 2012

Active mlearning opportunities offered by a prototype template of a new web-based SBLi™ interface for smartphones.

IJMLO, 2012

Some new results on decidability for elementary algebra and geometry.

Ann. Pure Appl. Logic, 2012

Iterative Design and Delivery of High Impact, Multiple Platform, Scenario-based Interactive Mobile Learning Activities in the Health Sciences.

Proceedings of the 11th International Conference on Mobile and Contextual Learning, 2012

2011

Formal Verification.

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

A formal proof of Pick's Theorem.

Mathematical Structures in Computer Science, 2011

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

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

The Contribution of NEISAS to EP3R.

Proceedings of the Critical Information Infrastructure Security, 2011

2010

A Revision of the Proof of the Kepler Conjecture.

Discrete & Computational Geometry, 2010

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

Comput. J., 2010

A k-12 college partnership.

Proceedings of the 41st ACM technical symposium on Computer science education, 2010

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

Proceedings of the Mathematical Software, 2010

2009

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

IEEE Trans. Computers, 2009

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

J. Formalized Reasoning, 2009

Formalizing an Analytic Proof of the Prime Number Theorem.

J. Autom. Reasoning, 2009

HOL Light: An Overview.

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

Without Loss of Generality.

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

Decimal Transcendentals via Binary.

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

Fast and Accurate Bessel Function Computation.

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

Handbook of Practical Logic and Automated Reasoning.

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

2008

Theorem Proving for Verification (Invited Tutorial).

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

2007

Verifying Nonlinear Real Formulas Via Sums of Squares.

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

Location and Format Independent Distributed Annotations for Collaborative Research.

Proceedings of the Research and Advanced Technology for Digital Libraries, 2007

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

Proceedings of the Automated Deduction, 2007

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

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

A Short Survey of Automated Reasoning.

Proceedings of the Algebraic Biology, Second International Conference, 2007

2006

HOL.

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

Floating-Point Verification Using Theorem Proving.

Proceedings of the Formal Methods for Hardware Verification, 2006

A curated harvesting approach to establishing a multi-protocol online subject portal.

Proceedings of the ACM/IEEE Joint Conference on Digital Libraries, 2006

Towards Self-verification of HOL Light.

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

2005

A HOL Theory of Euclidean Space.

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

Floating-Point Verification.

Proceedings of the FM 2005: Formal Methods, 2005

A Proof-Producing Decision Procedure for Real Arithmetic.

Proceedings of the Automated Deduction, 2005

2003

Formal Verification of Square Root Algorithms.

Formal Methods in System Design, 2003

Intel® Itanium® floating-point architecture.

Proceedings of the 2003 workshop on Computer architecture education, 2003

Formal Verification at Intel.

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

Isolating Critical Cases for Reciprocals Using Integer Factorization.

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

2002

Scientific computing on the Itanium® processor.

Scientific Programming, 2002

Enabling Hardware Verification through Design Changes.

Proceedings of the Formal Methods and Software Engineering, 2002

2001

Scientific computing on the Itanium processor.

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

2000

Formal Verification of IA-64 Division Algorithms.

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

Formal Verification of Floating Point Trigonometric Functions.

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

High-Level Verification Using Theorem Proving and Formalized Mathematics.

Proceedings of the Automated Deduction, 2000

1999

A Machine-Checked Theory of Floating Point Arithmetic.

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

1998

A Skeptic's Approach to Combining HOL and Maple.

J. Autom. Reasoning, 1998

The Gergonne p-pile Problem and the Dynamics of the Function x | => (x + r)/p.

Discrete Applied Mathematics, 1998

Formalizing Dijkstra.

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

Formalizing Basic First Order Model Theory.

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

Theorem proving with the real numbers.

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

1997

Verifying the Accuracy of Polynomial Approximations in HOL.

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

Floating Point Verification in HOL Light: The Exponential Function.

Proceedings of the Algebraic Methodology and Software Technology, 1997

1996

On Almost Cylindrical Languages and the Decidability of the D0L and PWD0L Primitivity Problems.

Theor. Comput. Sci., 1996

Proof Style.

Proceedings of the Types for Proofs and Programs, 1996

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

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

A Mizar Mode for HOL.

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

HOL Light: A Tutorial Introduction.

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

Optimizing Proof Search in Model Elimination.

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

1995

Dynamical Properties of PWD0L Systems.

Theor. Comput. Sci., 1995

Inductive Definitions: Automation and Application.

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

Floating Point Verification in HOL.

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

1994

Morphic Congruences and D0L Languages.

Theor. Comput. Sci., 1994

Binary Decision Diagrams as a HOL Derived Rule.

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

1993

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

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

A HOL Decision Procedure for Elementary Real Algebra.

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

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

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

1992

Constructing the real numbers in HOL.

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

Experience with Embedding Hardware Description Languages in HOL.

Proceedings of the Theorem Provers in Circuit Design, 1992