``My'' Best Ideas

Here are the technical achievements of which I am most proud. I think such a list gives more insight into my research than, say, the traditional ``Honors and Awards'' section of a resume.

None of this work can be considered mine alone.

Bob Boyer and Matt Kaufmann have been especially influential, even in work not bearing their names. In addition, my colleagues at CLI, my students, and the many users of Nqthm and ACL2 have been key players and I am grateful to all of them. Here are the mechanically checked proofs of which I'm most proud (counting only the ones where I played a key role): There are many other wonderful Nqthm- and ACL2-checked proofs done by others.