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

The 1973 Edinburgh Pure Lisp Theorem Prover (PLTP)
The Boyer-Moore Theorem Prover (NQTHM)
A Computational Logic for Applicative Common Lisp (ACL2)
The Linear Time Majority Vote Algorithm
The Boyer-Moore Fast String Searching Algorithm
Structure Sharing
Text Representation in Word Processing
Floyd-Hoare-style code proofs with Operational Semantics

Here are the mechanically checked proofs of which I'm most proud (counting only the ones where I played a key role):

Correctness of the AMD5k86 Floating-Point Division
A Model of Asynchronous Communication and the Correctness of the Biphase Mark Protocol
Piton and the CLI stack

There are many other wonderful Nqthm- and ACL2-checked proofs done by others.

[Home]