[TYPES] ACL2 Workshop

[Matt Kaufmann]

[Prologue:

  The announcement below may be of interested to those on the types list,
  although the only connection that comes to mind between ACL2 and types is
  that ACL2's language (applicative Common Lisp) is typeless (!), but users can
  specify and prove arbitrary input conditions, as described here:

  http://www.cs.utexas.edu/users/moore/acl2/v2-8/Guards.html
  http://www.cs.utexas.edu/users/moore/acl2/v2-8/GUARD.html

End of prologue.]

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)