The submissions Web page is here. Please read the following before submitting your paper.

Submissions must be made electronically in PDF format. Submissions must use the ACM SIG Proceedings format with letter-size paper (see http://www.acm.org/sigs/pubs/proceed/template.html).

Two categories of papers will be accepted: long (at most 10 pages) and short (at most 4 pages). Note that the current paper format is much more compact than the LNCS format we used in the past! Authors can assume that the workshop audience has a working knowledge of ACL2's syntax, basic commands, and modeling techniques. Papers should contain a short abstract of approximately 150 words clearly stating the contribution of the submission. Authors of accepted papers are required to give a presentation at the workshop. We expect to provide workshop proceedings and to include these proceedings in the ACM digital library.

Papers should be self-contained, but, as has been the case traditionally (and where applicable), we strongly encourage authors to provide ACL2 "books" or script files that provide full details, along with instructions for how to process these books with ACL2. The submission guidelines for supporting materials, which we strongly recommend you adhere to, can be found here. You should provide your supporting materials as a single gzipped or zipped tarball (with extension .tgz or .zip, respectively) using the paper submissions Web page. A template gzipped tarball can be found here and a template zipped tarball can be found here. For accepted papers, these books will be mirrored on the ACL2 home page and included in future ACL2 distributions.