Greetings [and apologies if you get multiple copies]: The fifth ACL2 Workshop will be held November 18-19, 2004, in Austin Texas, USA, in conjunction with (and immediately following) FMCAD. We invite users of ACL2, users of other theorem provers, and persons interested in the applications of theorem proving technology to attend. ACL2 is a state-of-the-art automated reasoning system, which grew out of the Boyer-Moore theorem prover and has been used successfully on a number of industrial and academic projects. ACL2 is described at http://www.cs.utexas.edu/users/moore/acl2. The ACL2 workshops provide a forum for the presentation and discussion of projects using ACL2 as well as the evolution of the tool. Topics include the following. o applications of the theorem prover o improvements and extensions to the theorem prover o comparisons of ACL2 to other theorem provers, programming languages, or specification languages o solved challenge problems for ACL2 users (especially challenges that help newcomers learn the system) o implementations connecting ACL2 and other systems For more information, including a call for papers, see: http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/ Relevant dates are as follows: Submission Deadline: July 26, 2004 Acceptance Notification: August 23, 2004 Registration without late fee: October 4, 2004 Workshop: November 18-19, 2004 Regards, Matt Kaufmann and J Moore (Organizing Committee)