[PRL] NEPLS VS. ACL2s

[Christine Hang]

Hi All,

I noticed that Peter's ACL2s talk scheduled for this Thursday at the  
PhD seminar conflicts with the upcoming NEPLS. I am assuming Peter's  
talk is of interest to some of the PRL folks (see the abstract  
below), and it is highly likely that these PRL folks will constitute  
the majority of the audience. So, I would like to get a rough idea on  
how many PL people will be affected by the conflict. So, if you are  
going to the NEPLS but want to attend the ACL2s talk as well, please  
email me. If enough people reply, we could consider the possibility  
of rescheduling the ACL2s talk.

-- Christine


ABSTRACT

ACL2 is the latest inception of the Boyer-Moore theorem prover,
the 2005 recipient of the ACM Software System Award.  In the
hands of experts it feels like a finely tuned race car, and it
has been used to prove some of the most complex theorems ever
proved about commercially designed systems.  Unfortunately, ACL2
has a steep learning curve. Thus, novices tend have a very
different experience: they crash and burn.

As part of a project to make ACL2 and formal reasoning accessible
to the masses, we have developed ACL2s: "The ACL2 Sedan".  ACL2s is
designed around natural interface abstractions and implemented
without leaks; thus, novices find the tool intuitive and robust, and
experienced users find it convenient.  We have also implemented
features for supporting the learning process, but the eventual goal
is to develop a tool that is "self-teaching."  One day it should be
possible for an undergraduate to sit down and play with our tool and
learn how to write and reason about programs in ACL2.
-------------- next part --------------
HTML attachment scrubbed and removed