Fifth International Workshop on the ACL2 Theorem Prover
and Its Applications (ACL2-2004)

As always, supporting materials (which are generally certifiable books) can be quite useful to readers of papers submitted to ACL2 workshops. If you submit them, it will be assumed (unless told otherwise) that the author(s) do not mind if such materials are eventually distributed with ACL2 workshop materials, where minor revisions are made from time to time so that they continue to work with new releases of ACL2.

If you submit supporting materials, it would be helpful (though this is optional) if you'd (1) develop your books using relative pathnames or :dir :system in your include-book forms, and (2) use the standard Makefile, which you can do as follows. First download this file:


Save this tar file to directory acl2-sources/books/, and then in that directory execute:

tar xvf support-2004.tar

This will create directory acl2-sources/books/workshops/2004/matt/support/. Change "matt" to your name. The Makefile in support/ has comments that you may find helpful. For more complex examples, download the previous workshops from and gunzip/untar in acl2-sources/books/.

Feel free to ask Matt Kaufmann for help with this process.