Computer Science Colloquium
Programming Languages and Automated Theorem Proving
Aaron Stump
Washington University
Friday, October 27, 2006, 2006 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 100121185
Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html
Hosts:
Clark Barrettbarrett@cs.nyu.edu, (212) 9983105
Abstract
In this talk I present two new examples of the long and
fruitful interplay between Programming Languages (PL) and Automated
Theorem Proving (ATP). The first example concerns machinechecked
proofs of properties of programming languages, such as type safety.
Typical current papers in PL conferences require many pages of detailed
proofs to establish the paper's theorems. An alternative being actively
explored is to formalize such proofs in a theorem prover. Advantages of
formalization include increased confidence in the theorems' correctness,
and the promise of extracting verified implementations of language tools
(e.g., type checkers) from the formal development. One technical
problem is handling language constructs that bind variables. I describe
my current work on a library called CTILIB for the Coq theorem prover,
which provides a generic treatment of terms with binders. The central
idea is the semantic notion of contextual term interpretation ("CTI"),
which supports recursive definitions over terms with binders. Any
function definable by CTI enjoys properties, proved once and for all in
the library, such as permutation of the context and a substitution
lemma. This generic support for binders decreases the burden of proof
for particular programming languages.
The second example of the interplay between PL and ATP is a new approach
to reflective theorem proving. The soundness of many contemporary
theorem provers depends on a very small trusted core: implementation of
a small set of axioms and inference rules for higherorder logic
provers, or implementation of a small core type theory for provers like
Coq. Any bugs in the rest of the typically very large (127kloc of ML
for Coq 8.0) code base do not compromise soundness. But there is a
conundrum: provers like Coq provide a program verification environment,
and yet we have 127kloc of unverified code. We cannot apply the one to
the other. I show work in progress to solve this problem by
bootstrapping the program verification environment. The central idea is
to base the prover on a logic for evaluation of (a novel kind of)
reflective programs. A proof checker for this logic can then be written
as such a reflective program. Thus, the proof checker can check proofs
about its own executions. So the proof checker can allow itself to be
extended with new, untrusted reasoning principles (e.g., tautology
checkers) by requiring a proof that shows: if the new reasoning
principle says a formula is valid, then there exists a proof that the
unextended proof checker would accept as a proof of that formula.
BIO
Aaron Stump's received his PhD in Computer Science from Stanford
University in 2002. His primary research interests are in computational
logic, automated reasoning, and programming languages theory.
Refreshments will be served
top  contact webmaster@cs.nyu.edu
