``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.