Date: Mon, 31 Jul 2006 18:24:12 -0500
From: Jared Davis

Hi,

Note: I accidentally sent this same abstract out awhile ago.  This time it's for 
real. :)

At this week's ACL2 meeting, I'll talk about adding a ``computation'' rule to 
Milawa, the reflective proof checker I have been developing.  This rule allows 
me to conclude that a ground term is equal to its computed value.  For example, 
(fib 2) = 2, (integerp (fib 10)) = t, and so forth.

I plan to talk about the following topics in detail:

   (1) The definition of formal proofs and my core proof checker,
   (2) How derived rules of inference can be used to construct proofs,
   (3) My general-purpose evaluation function,
   (4) Proving (in ACL2) that the evaluator is sound, and
   (5) Generating formal proofs of computations for bootstrapping.

I hope this will be an interesting demonstration of how my program can be
extended with a nontrivial and useful capability.  I'll also talk about how
I have been able to use this evaluator to develop a simple rewriter.

Thanks,
    Jared