| 2009 |
|---|
| 54 | EE | 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) |
| 2008 |
|---|
| 53 | EE | John Harrison:
Theorem Proving for Verification (Invited Tutorial).
CAV 2008: 11-18 |
| 2007 |
|---|
| 52 | EE | John Harrison:
A Short Survey of Automated Reasoning.
AB 2007: 334-349 |
| 51 | EE | John Harrison:
Automating Elementary Number-Theoretic Proofs Using Gröbner Bases.
CADE 2007: 51-66 |
| 50 | EE | Fabio Corubolo,
Paul B. Watry,
John Harrison:
Location and Format Independent Distributed Annotations for Collaborative Research.
ECDL 2007: 495-498 |
| 49 | EE | 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 |
| 48 | EE | John Harrison:
Verifying Nonlinear Real Formulas Via Sums of Squares.
TPHOLs 2007: 102-118 |
| 47 | EE | John Harrison:
Floating-Point Verification.
J. UCS 13(5): 629-638 (2007) |
| 2006 |
|---|
| 46 | | Dima Grigoriev,
John Harrison,
Edward A. Hirsch:
Computer Science - Theory and Applications, First International Computer Science Symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8-12, 2006, Proceedings
Springer 2006 |
| 45 | EE | John Harrison:
Towards Self-verification of HOL Light.
IJCAR 2006: 177-191 |
| 44 | EE | Robert Sanderson,
John Harrison,
Clare Llewellyn:
A curated harvesting approach to establishing a multi-protocol online subject portal.
JCDL 2006: 355 |
| 43 | EE | John Harrison:
Floating-Point Verification Using Theorem Proving.
SFM 2006: 211-242 |
| 42 | EE | John Harrison,
Konrad Slind,
Rob Arthan:
HOL.
The Seventeen Provers of the World 2006: 11-19 |
| 41 | EE | 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) |
| 2005 |
|---|
| 40 | EE | Sean McLaughlin,
John Harrison:
A Proof-Producing Decision Procedure for Real Arithmetic.
CADE 2005: 295-314 |
| 39 | EE | John Harrison:
Floating-Point Verification.
FM 2005: 529-532 |
| 38 | EE | John Harrison:
A HOL Theory of Euclidean Space.
TPHOLs 2005: 114-129 |
| 2003 |
|---|
| 37 | EE | John Harrison:
Isolating Critical Cases for Reciprocals Using Integer Factorization.
IEEE Symposium on Computer Arithmetic 2003: 148-157 |
| 36 | EE | John Harrison:
Formal Verification at Intel.
LICS 2003: 45- |
| 35 | EE | John Harrison:
Formal Verification of Square Root Algorithms.
Formal Methods in System Design 22(2): 143-153 (2003) |
| 2002 |
|---|
| 34 | EE | Amr T. Abdel-Hamid,
Sofiène Tahar,
John Harrison:
Enabling Hardware Verification through Design Changes.
ICFEM 2002: 459-470 |
| 33 | | Bruce Greer,
John Harrison,
Greg Henry,
Wei Li,
Peter Tang:
Scientific computing on the Itanium® processor.
Scientific Programming 10(4): 329-337 (2002) |
| 2001 |
|---|
| 32 | EE | Bruce Greer,
John Harrison,
Greg Henry,
Wei Li,
Peter Tang:
Scientific computing on the Itanium processor.
SC 2001: 41 |
| 2000 |
|---|
| 31 | | Mark Aagaard,
John Harrison:
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings
Springer 2000 |
| 30 | | John Harrison:
High-Level Verification Using Theorem Proving and Formalized Mathematics.
CADE 2000: 1-6 |
| 29 | EE | John Harrison:
Formal Verification of Floating Point Trigonometric Functions.
FMCAD 2000: 217-233 |
| 28 | | John Harrison:
Formal Verification of IA-64 Division Algorithms.
TPHOLs 2000: 233-251 |
| 27 | | John Harrison:
Floating Point Verification in HOL Light: The Exponential Function.
Formal Methods in System Design 16(3): 271-305 (2000) |
| 1999 |
|---|
| 26 | EE | John Harrison:
A Machine-Checked Theory of Floating Point Arithmetic.
TPHOLs 1999: 113-130 |
| 1998 |
|---|
| 25 | | John Harrison:
Formalizing Basic First Order Model Theory.
TPHOLs 1998: 153-170 |
| 24 | | John Harrison:
Formalizing Dijkstra.
TPHOLs 1998: 171-188 |
| 23 | EE | 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) |
| 22 | | John Harrison,
Laurent Théry:
A Skeptic's Approach to Combining HOL and Maple.
J. Autom. Reasoning 21(3): 279-294 (1998) |
| 1997 |
|---|
| 21 | | John Harrison:
Floating Point Verification in HOL Light: The Exponential Function.
AMAST 1997: 246-260 |
| 20 | | John Harrison:
Verifying the Accuracy of Polynomial Approximations in HOL.
TPHOLs 1997: 137-152 |
| 1996 |
|---|
| 19 | | 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
Springer 1996 |
| 18 | | John Harrison:
Optimizing Proof Search in Model Elimination.
CADE 1996: 313-327 |
| 17 | | John Harrison:
HOL Light: A Tutorial Introduction.
FMCAD 1996: 265-269 |
| 16 | | John Harrison:
A Mizar Mode for HOL.
TPHOLs 1996: 203-220 |
| 15 | | John Harrison:
Stålmarck's Algorithm as a HOL Derived Rule.
TPHOLs 1996: 221-234 |
| 14 | | John Harrison:
Proof Style.
TYPES 1996: 154-172 |
| 13 | EE | 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) |
| 1995 |
|---|
| 12 | | John Harrison:
Floating Point Verification in HOL.
TPHOLs 1995: 186-199 |
| 11 | | John Harrison:
Inductive Definitions: Automation and Application.
TPHOLs 1995: 200-213 |
| 10 | | John Harrison:
Binary Decision Diagrams as a HOL Derived Rule.
Comput. J. 38(2): 162-170 (1995) |
| 9 | EE | John Harrison:
Dynamical Properties of PWD0L Systems.
Theor. Comput. Sci. 143(2): 269-284 (1995) |
| 1994 |
|---|
| 8 | | John Harrison:
Binary Decision Diagrams as a HOL Derived Rule.
TPHOLs 1994: 254-268 |
| 7 | | John Harrison:
Constructing the Real Numbers in HOL.
Formal Methods in System Design 5(1/2): 35-59 (1994) |
| 6 | | John Harrison:
Morphic Congruences and D0L Languages.
Theor. Comput. Sci. 134(2): 537-544 (1994) |
| 1993 |
|---|
| 5 | | John Harrison,
Laurent Théry:
Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.
HUG 1993: 174-184 |
| 4 | | John Harrison:
A HOL Decision Procedure for Elementary Real Algebra.
HUG 1993: 426-435 |
| 3 | | John Harrison,
Laurent Théry:
Reasoning About the Reals: The Marriage of HOL and Maple.
LPAR 1993: 351-353 |
| 1992 |
|---|
| 2 | | Richard J. Boulton,
Andrew Gordon,
Michael J. C. Gordon,
John Harrison,
John Herbert,
John Van Tassel:
Experience with Embedding Hardware Description Languages in HOL.
TPCD 1992: 129-156 |
| 1 | | John Harrison:
Constructing the real numbers in HOL.
TPHOLs 1992: 145-164 |
