From: "Jared C. Davis"
Subject: This Halloween in ACL2

Hi,

This week the ACL2 meeting will be back to normal, and I'll be giving
a follow-up talk from my proposal.  My tentative plan is to show you:

1. The ACL2/Milawa connection:  What's involved in the ACL2 model of
Milawa, and how do I translate ACL2 proofs into Milawa proofs?  How
much work is it to write proofs in Milawa, and how do I interact with
the system?

2. The "big switch" event that I use to install a new proof checker:
How it is implemented, why is it sensible, and what you have to prove
to use it.  Also, how do I decide what goes into each level, and where
am I trying to head with the next levels?

3. Some useful tools that I've used or developed, including the OMake
build system, a "provisional certification" system that (greatly)
increases how many books I can "certify" in parallel, and "addjob", a
program I've written that lets me use several machines to build my
books.

But I'm also happy to go into more depth on anything else you'd like
to hear more about.

Hope to see you there,

   Jared