From: "Jared C. Davis"
Date: Mon, 14 Sep 2009 22:47:04 -0500
Subject: [acl2-mtg] This week in ACL2


Hi,

At this week's ACL2 seminar I'll give a practice talk for my defense
(which is this Friday).

I've included the abstract, below.  Since there will be some extra
time I will be happy to answer any hard questions, but please save any
easy questions for Friday. :)

Hope to see you there,

Jared


Ph.D. Final Oral Defense: Jared Davis

Date:  September 18
Location: TAY 3.128
Time: 12:00 Noon
Supervising Professor:  J Moore

Title:  A Self-Verifying Theorem Prover

Abstract:

Programs have precise semantics, so we can use mathematical proof
to establish their properties.  These proofs are often too large
to validate with the usual "social process" of mathematics, so
instead we create and check them with theorem-proving software.
This software must be advanced enough to make the proof process
tractable, but this very sophistication casts doubt upon the
whole enterprise: who verifies the verifier?

We begin with a simple proof checker, Level 1, that only accepts
proofs composed of the most primitive steps, like Instantiation
and Cut.  This program is so straightforward the ordinary, social
process can establish its soundness and the consistency of the
logical theory it implements (so we know theorems are "always
true").

Next, we develop a series of increasingly capable proof checkers,
Level 2, Level 3, etc.  Each new proof checker accepts new kinds
of proof steps which were not accepted in the previous levels.
By taking advantage of these new proof steps, higher-level proofs
can be more concise than lower-level proofs, and can take less
time to construct and check.  Our highest-level proof checker,
Level 11, can be thought of as a simplified version of the ACL2
or NQTHM theorem provers.  One contribution of this work is to
show how such systems can be verified.

We say Level n is sound if, whenever it accepts a proof of some
formula, phi, there exists a Level 1 proof of phi.  To establish
that the Level 11 proof checker can be trusted, we first use it,
without trusting it, to prove that every level is sound.  We then
mechanically translate the Level 11 proof for each Level n into a
Level n-1 proof.  That is, we create a Level 1 proof of soundness
for Level 2, a Level 2 proof of soundness for Level 3, and so on.
This layering shows that each level can be trusted, and allows us
to manage the sizes of these soundness proofs.

In this way, our system proves its own soundness, and trusting
the entire system only requires us to trust Level 1.