(extended abstract)

I’ve always been interested in using theorem provers both for “practical ” applications in formally verifying computer systems, and for the “pure ” formalization of traditional mathematical proofs. I particularly like situations where there is an interplay between the two. For example, in my PhD thesis [5], written under Mike Gordon’s supervision, I developed a formalization of some elementary real analysis. This was subsequently used in very practical verification applications [6], where in fact I even needed to for-malize more pure mathematics, such as power series for the cotangent function and basic theorems about diophantine approximation. I first joined Mike Gordon’s HVG (Hardware Verification Group) to work on an embedding in HOL of the hardware description language ELLA. Mike had already directed several similar research projects, and one concept first clearly articulated as a result of these activities was the now-standard distinction between ‘deep ’ and ‘shallow’ embeddings of languages [3]. Since I was interested in formalizing real analysis, Mike encouraged me to direct my attention to case studies involving arithmetic, and this was the starting-point for my subsequent research. Right from the beginning, Mik