After completing his PhD research in 1995, John Harrison spent a very enjoyable year at Åbo Akademi University and Turku Centre for Computer Science (TUCS) in Turku, Finland, where he was a member of Ralph Back's Programming Methods Research Group. Among other activities, he championed the "declarative" proofs of the Mizar system and showed how these could be integrated into other theorem-provers, work subsequently taken up in DECLARE, Isar and other systems.
John Harrison then returned to Cambridge and worked on a formal model of floating-point arithmetic and its application to the verification of some realistic algorithms for transcendental functions. This work attracted the attention of Intel, and in 1998 John Harrison joined the company as a Senior Software Engineer specializing in the design and formal verification of mathematical algorithms. He has formally verified and in many cases designed or redesigned numerous algorithms for mathematical functions including division, square root and trigonometric functions.
In his limited spare time over the past 8 years, John Harrison has been working on a book giving a comprehensive introduction to automated theorem proving. He hopes that this book will finally reach publication in 2005, and the associated code is already available from his Web page.