Date: Mon, 12 May 2008 16:14:54 -0500
From: Jared C. Davis
Subject: This week in ACL2

Hi,

At this week's ACL2 meeting, I will give an informal Milawa talk & demo.

There are a few things I'd like to cover.

  - A simple demo of proving a couple of theorems in my system and of
    translating ACL2 proofs into Milawa.

  - A short tour of the extended proof checkers I have verified so far,
    focusing on what they do and why.

  - "Proof adaptors", a new idea which allows me to support extended
    proof checkers that take more arguments than the base proof checker.
    This lets me precompute various things that will be used throughout
    the proof, for instance, "all the function definitions I'm going to
    use are valid."

  - Using tables efficiently even when including uncertified books, via
    make-event, local, and program-mode wrappers.

  - Higher-ordery-ish things you can do with a magic evaluator (syntaxp,
    gather, ...)

I'm happy to go off on whatever tangents you like.

Cheers,

Jared