John Harrison

John Harrison: The HOL Light Theory of Euclidean Space. J. Autom. Reasoning 50(2): 173-190 (2013)

Robert Solovay, R. D. Arthan, John Harrison: Some new results on decidability for elementary algebra and geometry. Ann. Pure Appl. Logic 163(12): 1765-1802 (2012)

Trena M. Paulus, Gina Phipps, John Harrison, Mary Alice Varga: Re-envisioning instructional technology research in higher education environments: a content analysis of a grant program. J. Computing in Higher Education 24(3): 164-181 (2012)

Hartmuth Ernst, John Harrison, David Griffin: Iterative Design and Delivery of High Impact, Multiple Platform, Scenario-based Interactive Mobile Learning Activities in the Health Sciences. mLearn 2012: 240-243

John Harrison: A formal proof of Pick's Theorem. Mathematical Structures in Computer Science 21(4): 715-729 (2011)

Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell: Robin Milner 1934--2010: verification, languages, and concurrency. POPL 2011: 473-474

John Harrison: Formal Verification. Software and Systems Safety - Specification and Verification 2011: 103-157

Behzad Akbarpour, Amr T. 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)

Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller: A Revision of the Proof of the Kepler Conjecture. Discrete & Computational Geometry 44(1): 1-34 (2010)

John Harrison: A Formal Proof of Pick's Theorem - (Extended Abstract). ICMS 2010: 152-154

Stephen Cooper, Wanda Dann, John Harrison: A k-12 college partnership. SIGCSE 2010: 320-324

John Harrison: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press 2009, isbn 978-0-521-89957-4, pp. I-XIX, 1-681

John Harrison: Formalizing an Analytic Proof of the Prime Number Theorem. J. Autom. Reasoning 43(3): 243-261 (2009)

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)

John Harrison: Fast and Accurate Bessel Function Computation. IEEE Symposium on Computer Arithmetic 2009: 104-113

John Harrison: Decimal Transcendentals via Binary. IEEE Symposium on Computer Arithmetic 2009: 187-194

John Harrison: Without Loss of Generality. TPHOLs 2009: 43-59

John Harrison: HOL Light: An Overview. TPHOLs 2009: 60-66

Javier D. Bruguera, Marius Cornea, Debjit Das Sarma, John Harrison (Eds.): 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

John Harrison: Theorem Proving for Verification (Invited Tutorial). CAV 2008: 11-18

John Harrison: Floating-Point Verification. J. UCS 13(5): 629-638 (2007)

John Harrison: A Short Survey of Automated Reasoning. AB 2007: 334-349

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

John Harrison: Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. CADE 2007: 51-66

Fabio Corubolo, Paul B. Watry, John Harrison: Location and Format Independent Distributed Annotations for Collaborative Research. ECDL 2007: 495-498

John Harrison: Verifying Nonlinear Real Formulas Via Sums of Squares. TPHOLs 2007: 102-118

John Harrison: Towards Self-verification of HOL Light. IJCAR 2006: 177-191

Robert Sanderson, John Harrison, Clare Llewellyn: A curated harvesting approach to establishing a multi-protocol online subject portal. JCDL 2006: 355

John Harrison: Floating-Point Verification Using Theorem Proving. SFM 2006: 211-242

John Harrison, Konrad Slind, Rob Arthan: HOL. The Seventeen Provers of the World 2006: 11-19

Dima Grigoriev, John Harrison, Edward A. Hirsch (Eds.): Computer Science - Theory and Applications, First International Computer Science Symposium 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

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)

Sean McLaughlin, John Harrison: A Proof-Producing Decision Procedure for Real Arithmetic. CADE 2005: 295-314

John Harrison: Floating-Point Verification. FM 2005: 529-532

John Harrison: A HOL Theory of Euclidean Space. TPHOLs 2005: 114-129

John Harrison: Formal Verification of Square Root Algorithms. Formal Methods in System Design 22(2): 143-153 (2003)

John Harrison: Isolating Critical Cases for Reciprocals Using Integer Factorization. IEEE Symposium on Computer Arithmetic 2003: 148-157

John Harrison: Formal Verification at Intel. LICS 2003: 45-

Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Peter Tang: Scientific computing on the Itanium® processor. Scientific Programming 10(4): 329-337 (2002)

Amr T. Abdel-Hamid, Sofiène Tahar, John Harrison: Enabling Hardware Verification through Design Changes. ICFEM 2002: 459-470

Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Peter Tang: Scientific computing on the Itanium processor. SC 2001: 41

John Harrison: Floating Point Verification in HOL Light: The Exponential Function. Formal Methods in System Design 16(3): 271-305 (2000)

John Harrison: High-Level Verification Using Theorem Proving and Formalized Mathematics. CADE 2000: 1-6

John Harrison: Formal Verification of Floating Point Trigonometric Functions. FMCAD 2000: 217-233

John Harrison: Formal Verification of IA-64 Division Algorithms. TPHOLs 2000: 233-251

Mark Aagaard, John Harrison (Eds.): 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

John Harrison: A Machine-Checked Theory of Floating Point Arithmetic. TPHOLs 1999: 113-130

John Harrison: Theorem proving with the real numbers. CPHC/BCS distinguished dissertations, Springer 1998, isbn 978-3-540-76256-0, pp. I-XII, 1-186

John Harrison, Thomas Brennan, Steven Gapinski: The Gergonne p-pile Problem and the Dynamics of the Function x | => (x + r)/p. Discrete Applied Mathematics 82(1-3): 103-113 (1998)

John Harrison, Laurent Théry: A Skeptic's Approach to Combining HOL and Maple. J. Autom. Reasoning 21(3): 279-294 (1998)

John Harrison: Formalizing Basic First Order Model Theory. TPHOLs 1998: 153-170

John Harrison: Formalizing Dijkstra. TPHOLs 1998: 171-188

John Harrison: Floating Point Verification in HOL Light: The Exponential Function. AMAST 1997: 246-260

John Harrison: Verifying the Accuracy of Polynomial Approximations in HOL. TPHOLs 1997: 137-152

John Harrison: On Almost Cylindrical Languages and the Decidability of the D0L and PWD0L Primitivity Problems. Theor. Comput. Sci. 164(1&2): 29-40 (1996)

John Harrison: Optimizing Proof Search in Model Elimination. CADE 1996: 313-327

John Harrison: HOL Light: A Tutorial Introduction. FMCAD 1996: 265-269

John Harrison: A Mizar Mode for HOL. TPHOLs 1996: 203-220

John Harrison: Stålmarck's Algorithm as a HOL Derived Rule. TPHOLs 1996: 221-234

John Harrison: Proof Style. TYPES 1996: 154-172

Joakim von Wright, Jim Grundy, John Harrison (Eds.): 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

John Harrison: Binary Decision Diagrams as a HOL Derived Rule. Comput. J. 38(2): 162-170 (1995)

John Harrison: Dynamical Properties of PWD0L Systems. Theor. Comput. Sci. 143(2): 269-284 (1995)

John Harrison: Floating Point Verification in HOL. TPHOLs 1995: 186-199

John Harrison: Inductive Definitions: Automation and Application. TPHOLs 1995: 200-213

John Harrison: Constructing the Real Numbers in HOL. Formal Methods in System Design 5(1/2): 35-59 (1994)

John Harrison: Morphic Congruences and D0L Languages. Theor. Comput. Sci. 134(2): 537-544 (1994)

John Harrison: Binary Decision Diagrams as a HOL Derived Rule. TPHOLs 1994: 254-268

John Harrison, Laurent Théry: Reasoning About the Reals: The Marriage of HOL and Maple. LPAR 1993: 351-353

John Harrison, Laurent Théry: Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. HUG 1993: 174-184

John Harrison: A HOL Decision Procedure for Elementary Real Algebra. HUG 1993: 426-435

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

John Harrison: Constructing the real numbers in HOL. TPHOLs 1992: 145-164