(picture of me) John Harrison
Intel Corporation, RA2-406
2501 NW 229th Avenue
Hillsboro, OR 97124

work: +1 503 712-8451
fax: +1 503 264-1790

My book code now has an F# version
Thanks to Eric Taucher, Jack Pappas and Anh-Dung Phan.

(cover of HOPLAR)

I do formal verification at Intel Corporation. I specialize in verification of floating-point algorithms and other mathematical software, but I'm interested in all aspects of theorem proving and verification. I'm also interested in floating-point arithmetic itself, and contributed to the revision process that led to the new IEEE 754 floating-point standard. Before joining Intel in 1998, I was a member of the Automated Reasoning Group at the Computer Laboratory of the University of Cambridge. I worked as a Research Associate and PhD student there, supervised by Mike Gordon, and after a spending a year in the Department of Computer Science of Åbo Akademi University in Finland, returned to Cambridge as a Research Associate working on Floating Point Verification.

I helped to organize the last IEEE ARITH (computer arithmetic) conference in Portland, OR, and took part in the Hanoi Workshop on Formal Proof and the Flyspeck Project. I've been on the PC for several recent and forthcoming conferences connected with automated reasoning and verification, symbolic computation and computer arithmetic: I'm also on the editorial board of the Journal of Automated Reasoning. Consider submitting a paper, or telling us about any relevant books (I'm book review editor).

Page last updated Friday 4th January 2013.