John Harrison - RankMe

72 papers A* 3A 6B 5C 6Misc 2Journal 20Unranked 23

Year	Rank	Type	Title / Venue / Authors
2019	B	`ed.`	10th International Conference on Interactive Theorem Proving, ITP 2019, Portland, OR, USA, September 9-12, 2019 ITP John Harrison, John O'Leary, Andrew Tolmach
2016	J	`jnl`	Preface: Twenty Years of the QED Manifesto. J. Formaliz. Reason. John Harrison, Josef Urban, Freek Wiedijk
2015	J	`jnl`	A formal proof of the Kepler conjecture. CoRR Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller
2015	J	`jnl`	Formal Proofs of Hypergeometric Sums - Dedicated to the memory of Andrzej Trybulec. J. Autom. Reason. John Harrison
2014	J	`jnl`	Formally verified mathematics. Commun. ACM Jeremy Avigad, John Harrison
2014	—	`ch.`	History of Interactive Theorem Proving. Computational Logic John Harrison, Josef Urban, Freek Wiedijk
2013	J	`jnl`	The HOL Light Theory of Euclidean Space. J. Autom. Reason. John Harrison
2012	J	`jnl`	Some new results on decidability for elementary algebra and geometry. Ann. Pure Appl. Log. Robert Solovay, R. D. Arthan, John Harrison
2011	J	`jnl`	A formal proof of Pick's Theorem. Math. Struct. Comput. Sci. John Harrison
2011	—	`ch.`	Formal Verification. Software and Systems Safety - Specification and Verification John Harrison
2011	A*	`conf`	Robin Milner 1934--2010: verification, languages, and concurrency. POPL Andrew D. Gordon, Robert Harper, John Harrison, Alan Jeffrey, Peter Sewell
2010	—	`conf`	A Formal Proof of Pick's Theorem - (Extended Abstract). ICMS John Harrison
2010	J	`jnl`	A Revision of the Proof of the Kepler Conjecture. Discret. Comput. Geom. Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, Roland Zumkeller
2010	J	`jnl`	Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. Comput. J. Behzad Akbarpour, Amr Talaat Abdel-Hamid, Sofiène Tahar, John Harrison
2009	C	`ed.`	19th IEEE Symposium on Computer Arithmetic, ARITH 2009, Portland, Oregon, USA, 9-10 June 2009 IEEE Symposium on Computer Arithmetic Javier D. Bruguera, Marius Cornea, Debjit Das Sarma, John Harrison
2009	J	`jnl`	A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format. IEEE Trans. Computers Marius Cornea, John Harrison, Cristina Anderson, Ping Tak Peter Tang, Eric Schneider, Evgeny Gvozdev
2009	J	`jnl`	A formalized proof of Dirichlet's theorem on primes in arithmetic progression. J. Formaliz. Reason. John Harrison
2009	C	`conf`	Decimal Transcendentals via Binary. IEEE Symposium on Computer Arithmetic John Harrison
2009	C	`conf`	Fast and Accurate Bessel Function Computation. IEEE Symposium on Computer Arithmetic John Harrison
2009	J	`jnl`	Formalizing an Analytic Proof of the Prime Number Theorem. J. Autom. Reason. John Harrison
2009	—	`conf`	HOL Light: An Overview. TPHOLs John Harrison
2009	—	`book`	Handbook of Practical Logic and Automated Reasoning. John Harrison
2009	—	`conf`	Without Loss of Generality. TPHOLs John Harrison
2008	A*	`conf`	Theorem Proving for Verification (Invited Tutorial). CAV John Harrison
2007	—	`conf`	A Short Survey of Automated Reasoning. AB John Harrison
2007	C	`conf`	A Software Implementation of the IEEE 754R Decimal Floating-Point Arithmetic Using the Binary Encoding Format. IEEE Symposium on Computer Arithmetic Marius Cornea, Cristina Anderson, John Harrison, Ping Tak Peter Tang, Eric Schneider, Charles Tsen
2007	A	`conf`	Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. CADE John Harrison
2007	J	`jnl`	Floating-Point Verification. J. Univers. Comput. Sci. John Harrison
2007	—	`conf`	Verifying Nonlinear Real Formulas Via Sums of Squares. TPHOLs John Harrison
2006	Misc	`ed.`	Computer Science - Theory and Applications, First International Symposium on Computer Science in Russia, CSR 2006, St. Petersburg, Russia, June 8-12, 2006, Proceedings CSR Dima Grigoriev, John Harrison, Edward A. Hirsch
2006	—	`conf`	Floating-Point Verification Using Theorem Proving. SFM John Harrison
2006	—	`ch.`	HOL. The Seventeen Provers of the World John Harrison, Konrad Slind, Rob Arthan
2006	J	`jnl`	LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL) CoRR Christoph Benzmüller, John Harrison, Carsten Schürmann
2006	A	`conf`	Towards Self-verification of HOL Light. IJCAR John Harrison
2005	—	`conf`	A HOL Theory of Euclidean Space. TPHOLs John Harrison
2005	A	`conf`	A Proof-Producing Decision Procedure for Real Arithmetic. CADE Sean McLaughlin, John Harrison
2005	B	`conf`	Floating-Point Verification. FM John Harrison
2003	A*	`conf`	Formal Verification at Intel. LICS John Harrison
2003	J	`jnl`	Formal Verification of Square Root Algorithms. Formal Methods Syst. Des. John Harrison
2003	Misc	`conf`	Intel® Itanium® floating-point architecture. WCAE Marius Cornea, John Harrison, Ping Tak Peter Tang
2003	C	`conf`	Isolating Critical Cases for Reciprocals Using Integer Factorization. IEEE Symposium on Computer Arithmetic John Harrison
2002	C	`conf`	Enabling Hardware Verification through Design Changes. ICFEM Amr Talaat Abdel-Hamid, Sofiène Tahar, John Harrison
2002	J	`jnl`	Scientific computing on the Itanium® processor. Sci. Program. Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Ping Tak Peter Tang
2001	A	`conf`	Scientific computing on the Itanium processor. SC Bruce Greer, John Harrison, Greg Henry, Wei Wayne Li, Ping Tak Peter Tang
2000	J	`jnl`	Floating Point Verification in HOL Light: The Exponential Function. Formal Methods Syst. Des. John Harrison
2000	B	`conf`	Formal Verification of Floating Point Trigonometric Functions. FMCAD John Harrison
2000	—	`conf`	Formal Verification of IA-64 Division Algorithms. TPHOLs John Harrison
2000	A	`conf`	High-Level Verification Using Theorem Proving and Formalized Mathematics. CADE John Harrison
2000	—	`ed.`	Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings TPHOLs Mark D. Aagaard, John Harrison
1999	—	`conf`	A Machine-Checked Theory of Floating Point Arithmetic. TPHOLs John Harrison
1998	J	`jnl`	A Skeptic's Approach to Combining HOL and Maple. J. Autom. Reason. John Harrison, Laurent Théry
1998	—	`conf`	Formalizing Basic First Order Model Theory. TPHOLs John Harrison
1998	—	`conf`	Formalizing Dijkstra. TPHOLs John Harrison
1998	—	`book`	Theorem proving with the real numbers. John Harrison
1997	—	`conf`	Floating Point Verification in HOL Light: The Exponential Function. AMAST John Harrison
1997	—	`conf`	Verifying the Accuracy of Polynomial Approximations in HOL. TPHOLs John Harrison
1996	—	`conf`	A Mizar Mode for HOL. TPHOLs John Harrison
1996	B	`conf`	HOL Light: A Tutorial Introduction. FMCAD John Harrison
1996	A	`conf`	Optimizing Proof Search in Model Elimination. CADE John Harrison
1996	—	`conf`	Proof Style. TYPES John Harrison
1996	—	`conf`	Stålmarck's Algorithm as a HOL Derived Rule. TPHOLs John Harrison
1996	—	`ed.`	Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings TPHOLs Joakim von Wright, Jim Grundy, John Harrison
1995	J	`jnl`	Binary Decision Diagrams as a HOL Derived Rule. Comput. J. John Harrison
1995	—	`conf`	Floating Point Verification in HOL. TPHOLs John Harrison
1995	—	`conf`	Inductive Definitions: Automation and Application. TPHOLs John Harrison
1994	—	`conf`	Binary Decision Diagrams as a HOL Derived Rule. TPHOLs John Harrison
1994	J	`jnl`	Constructing the Real Numbers in HOL. Formal Methods Syst. Des. John Harrison
1993	—	`conf`	A HOL Decision Procedure for Elementary Real Algebra. HUG John Harrison
1993	—	`conf`	Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals. HUG John Harrison, Laurent Théry
1993	B	`conf`	Reasoning About the Reals: The Marriage of HOL and Maple. LPAR John Harrison, Laurent Théry
1992	—	`conf`	Constructing the real numbers in HOL. TPHOLs John Harrison
1992	—	`conf`	Experience with Embedding Hardware Description Languages in HOL. TPCD Richard J. Boulton, Andrew D. Gordon, Michael J. C. Gordon, John Harrison, John Herbert, John Van Tassel