(picture of me) John Harrison
AWS Elemental
1320 SW Broadway, Suite 400
Portland, OR 97201


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 am a member of the Automated Reasoning Group at Amazon Web Services, after being previously at Intel Corporation. I'm interested in all aspects of theorem proving and verification and at Intel focused especially on numerical and mathematical applications. 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 Wednesday 17th January 2018.