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