The SCEAS System
Navigation Menu
Introduction
Collection Based
Clustering
Ranking
Paper Based
Journals
Conferences
DB Status
Statistics
Search

Search the dblp DataBase

Title:
Author:
John Harrison: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

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

  49. Decimal Transcendentals via Binary. [Citation Graph (, )][DBLP]


  50. Fast and Accurate Bessel Function Computation. [Citation Graph (, )][DBLP]


  51. Theorem Proving for Verification (Invited Tutorial). [Citation Graph (, )][DBLP]


  52. A Formal Proof of Pick's Theorem - (Extended Abstract). [Citation Graph (, )][DBLP]


  53. A k-12 college partnership. [Citation Graph (, )][DBLP]


  54. HOL Light: An Overview. [Citation Graph (, )][DBLP]


  55. Without Loss of Generality. [Citation Graph (, )][DBLP]


  56. Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. [Citation Graph (, )][DBLP]


  57. A Revision of the Proof of the Kepler Conjecture. [Citation Graph (, )][DBLP]


Search in 0.003secs, Finished in 0.306secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
Introduction Collection Based Clustering Ranking Paper Based Journals Conferences DB Status Statistics Search
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002