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