John Harrison

	2011
69		Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell: Robin Milner 1934--2010: verification, languages, and concurrency. POPL 2011: 473-474
68		John Harrison: Formal Verification. Software and Systems Safety - Specification and Verification 2011: 103-157
67		John Harrison: A formal proof of Pick's Theorem. Mathematical Structures in Computer Science 21(4): 715-729 (2011)
	2010
66		John Harrison: A Formal Proof of Pick's Theorem - (Extended Abstract). ICMS 2010: 152-154
65		Stephen Cooper, Wanda Dann, John Harrison: A k-12 college partnership. SIGCSE 2010: 320-324
64		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)
63		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)
	2009
62		John Harrison: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press 2009: I-XIX, 1-681
61		Javier D. Bruguera, Marius Cornea, Debjit Das Sarma, John Harrison: 19th IEEE Symposium on Computer Arithmetic, ARITH 2009, Portland, Oregon, USA, 9-10 June 2009 IEEE Computer Society 2009
60		John Harrison: Fast and Accurate Bessel Function Computation. IEEE Symposium on Computer Arithmetic 2009: 104-113
59		John Harrison: Decimal Transcendentals via Binary. IEEE Symposium on Computer Arithmetic 2009: 187-194
58		John Harrison: Without Loss of Generality. TPHOLs 2009: 43-59
57		John Harrison: HOL Light: An Overview. TPHOLs 2009: 60-66
56		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)
55		John Harrison: Formalizing an Analytic Proof of the Prime Number Theorem. J. Autom. Reasoning 43(3): 243-261 (2009)
	2008
54		John Harrison: Theorem Proving for Verification (Invited Tutorial). CAV 2008: 11-18
	2007
53		John Harrison: A Short Survey of Automated Reasoning. AB 2007: 334-349
52		John Harrison: Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. CADE 2007: 51-66
51		Fabio Corubolo, Paul B. Watry, John Harrison: Location and Format Independent Distributed Annotations for Collaborative Research. ECDL 2007: 495-498
50		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
49		John Harrison: Verifying Nonlinear Real Formulas Via Sums of Squares. TPHOLs 2007: 102-118
48		John Harrison: Floating-Point Verification. J. UCS 13(5): 629-638 (2007)
	2006
47		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
46		John Harrison: Towards Self-verification of HOL Light. IJCAR 2006: 177-191
45		Robert Sanderson, John Harrison, Clare Llewellyn: A curated harvesting approach to establishing a multi-protocol online subject portal. JCDL 2006: 355
44		John Harrison: Floating-Point Verification Using Theorem Proving. SFM 2006: 211-242
43		John Harrison, Konrad Slind, Rob Arthan: HOL. The Seventeen Provers of the World 2006: 11-19
42		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
41		Sean McLaughlin, John Harrison: A Proof-Producing Decision Procedure for Real Arithmetic. CADE 2005: 295-314
40		John Harrison: Floating-Point Verification. FM 2005: 529-532
39		John Harrison: A HOL Theory of Euclidean Space. TPHOLs 2005: 114-129
	2003
38		John Harrison: Isolating Critical Cases for Reciprocals Using Integer Factorization. IEEE Symposium on Computer Arithmetic 2003: 148-157
37		John Harrison: Formal Verification at Intel. LICS 2003: 45-
36		John Harrison: Formal Verification of Square Root Algorithms. Formal Methods in System Design 22(2): 143-153 (2003)
	2002
35		Amr T. Abdel-Hamid, Sofiène Tahar, John Harrison: Enabling Hardware Verification through Design Changes. ICFEM 2002: 459-470
34		Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Peter Tang: Scientific computing on the Itanium® processor. Scientific Programming 10(4): 329-337 (2002)
	2001
33		Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Peter Tang: Scientific computing on the Itanium processor. SC 2001: 41
	2000
32		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
31		John Harrison: High-Level Verification Using Theorem Proving and Formalized Mathematics. CADE 2000: 1-6
30		John Harrison: Formal Verification of Floating Point Trigonometric Functions. FMCAD 2000: 217-233
29		John Harrison: Formal Verification of IA-64 Division Algorithms. TPHOLs 2000: 233-251
28		John Harrison: Floating Point Verification in HOL Light: The Exponential Function. Formal Methods in System Design 16(3): 271-305 (2000)
	1999
27		John Harrison: A Machine-Checked Theory of Floating Point Arithmetic. TPHOLs 1999: 113-130
	1998
26		John Harrison: Theorem proving with the real numbers. Springer 1998: I-XII, 1-186
25		John Harrison: Formalizing Basic First Order Model Theory. TPHOLs 1998: 153-170
24		John Harrison: Formalizing Dijkstra. TPHOLs 1998: 171-188
23		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		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		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 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
1		John Harrison: Constructing the real numbers in HOL. TPHOLs 1992: 145-164

Coauthor Index

1	Mark Aagaard	[32]
2	Amr T. Abdel-Hamid	[35] [64]
3	Behzad Akbarpour	[64]
4	Cristina Anderson	[50] [56]
5	Rob Arthan	[43]
6	Christoph Benzmüller (Christoph Benzmueller)	[42]
7	Richard J. Boulton	[2]
8	Thomas Brennan	[23]
9	Javier D. Bruguera	[61]
10	Stephen Cooper	[65]
11	Marius Cornea	[50] [56] [61]
12	Fabio Corubolo	[51]
13	Wanda Dann	[65]
14	Steven Gapinski	[23]
15	Andrew D. Gordon (Andy Gordon)	[2] [69]
16	Michael J. C. Gordon	[2]
17	Bruce Greer	[33] [34]
18	Dima Grigoriev	[47]
19	Jim Grundy	[19]
20	Evgeny Gvozdev	[56]
21	Thomas C. Hales	[63]
22	Robert Harper	[69]
23	Greg Henry	[33] [34]
24	John Herbert	[2]
25	Edward A. Hirsch	[47]
26	Alan Jeffrey	[69]
27	Wei Wayne Li	[33] [34]
28	Clare Llewellyn	[45]
29	Sean McLaughlin	[41] [63]
30	Tobias Nipkow	[63]
31	Steven Obua	[63]
32	Robert Sanderson	[45]
33	Debjit Das Sarma	[61]
34	Eric Schneider	[50] [56]
35	Carsten Schürmann	[42]
36	Peter Sewell	[69]
37	Konrad Slind	[43]
38	Sofiène Tahar	[35] [64]
39	Peter Tang	[33] [34]
40	Ping Tak Peter Tang	[50] [56]
41	John Van Tassel	[2]
42	Laurent Théry	[3] [5] [22]
43	Charles Tsen	[50]
44	Paul B. Watry	[51]
45	Joakim von Wright	[19]
46	Roland Zumkeller	[63]

Colors in the list of coauthors

Last update Thu May 31 18:55:10 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page