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.

• HOL Light theorem prover Now hosted on Github
• My papers and other publications Updated December 2015
• Slides from some of my recent talks Updated December 2015
• Code accompanying my recent book
• Errata for the book
• My 1996 functional programming course Russian version
• Detailed contact information

Page last updated Thursday 28th February 2019.