New Confluence URL

The wiki is now accessible through Please update your bookmarks and documentation accordingly.

Skip to end of metadata
Go to start of metadata

J. Strother Moore, the Moore in Boyer-Moore, just completed a two-days visit to Northeastern. He gave a talk, Machines Reasoning about Machines, complete with demo using the ACL2 theorem prover. ACL2 is a first-order theorem prover for proving equational properties of programs written in an applicative subset of Common Lisp. It is amazingly fast, and comes with a well-equipped library of theories to work with.

Fascinating work, if only because I am set to teach an undergraduate course using ACL2 next semester with Pete Manolios.

Now if we could just move the ACL2 technology to a typed language and extend it to higher-order, I'd be happy. (I know, I know, there are fundamental limitations re the latter, but still, even getting halfway there would be fun.)

Pete told me that the two books on ACL2:

  • Computer-Aided Reasoning: An Approach
  • Computer-Aided Reasoning: ACL2 Case Studies

are now available in paperback for a very reasonable fee.