A Computational Logic for Applicative Common Lisp (ACL2)

ACL2 is a direct descendent of the Boyer-Moore theorem prover, intended for large scale verification projects. ACL2 was created by Matt Kaufmann and J Moore, working from a kernel developed by Boyer and Moore. The key ideas in ACL2 are

I think it's really cool that the system is coded in its own logic. How many theorem provers can you say that about? How many 5 Mbyte applicative programs can you name?

ACL2 is quite young by Nqthm's standards. (The ACL2 Project was begun in 1989.) But it has been used to do some impressive things.

The comprehensive source for information about ACL2 is the ACL2 Home Page. Sources and documentation are freely distributed from there (under a 3-clause BSD license), as are many papers about ACL2 and its applications. In addition, the page links to many other books and papers and other ACL2-related resources.

[Best Ideas] [Publications] [Research] [Home]