(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
and the interactive part has an SML version
Thanks to Eric Taucher, Jack Pappas, Anh-Dung Phan, Anders Schlichtkrull and Jørgen Villadsen.

(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.

Page last updated Monday 19th June 2017.