Date: Tue, 27 Mar 2007 15:43:38 -0500 (CDT)
From: Jared C. Davis
To: acl2-mtg@lists.cc.utexas.edu
Subject: Change of plans, I'll be talking at tomorrow's meeting

Hi,

Sol and I have agreed to swap spots for our ACL2 presentations, so 
tomorrow I will be presenting instead of him.  Please disregard his
abstract.  Here's what I'll be talking about:

   Milawa: Tactics and Tracing

   Background.  Milawa is a new proof checker for an ACL2-like logic.
   The goal is to build a prover with a small, trusted core that can
   reflectively verify its own extensions.  I began by defining the
   core and many extensions in ACL2, and by using ACL2 to prove these
   extensions are sound.  The challenge is now to "port" these proofs
   into the core system.

   My talk will cover two key components of this effort: tactics and
   tracing.

   I'll begin by giving an overview of tactic systems in LCF-style
   theorem provers (e.g., HOL), and discussing how I've implemented
   tactics in my system.  I'll explain what a couple of my tactics
   do, and I'll then show you a demo of an interactive tactic
   interface which allows me to prove new theorems using tactics.

   I'll then talk about rewriter tracing.  This idea allows me to
   separate proof building from proof search in my rewriters, which
   considerably simplifies the proof of the rewriter's correctness
   and also has important efficiency benefits.

This is all very current work -- just last night I used the tactic
system to build my first inductive Milawa proof, natp-of-len -- so
I'm pretty excited. :)

Hope to see you there,

     Jared