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 10012-1185

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) 998-3105

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 machine-checked 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 CTI-LIB 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 higher-order 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