Princeton University
Computer Science Dept.

Seminar in Automated Theorem Proving Andrew Appel

Spring 1999

Automated (and semi-automated) theorem proving has been around for three decades. Now it's ripe for a killer app. Maybe that application is proof-carrying code, or maybe something else. Either way, the science of automated proving is interesting for its own sake. Let's learn how to do it.

The seminar will cover sequent logic, Prolog and lambdaProlog programming, hands-on practice proving things, and applications to proof-carrying code and mobile-code security.

General Information

Seminar: meets Fridays 2:00-4:00 in room 302.

Professor: Andrew Appel, 409 CS Building, 258-4627, appel@cs

Course structure

I'm on sabbatical, so I'm not going to teach this like a regular course. I'll deliver some lectures and provide a reading list to get you started, then you can work together to keep it going.

Running lambdaProlog

The Terzo implementation of lambdaProlog is installed locally on the Sparc machines as /usr/local/sml/bin/Terzo. See also The Terzo Home Page, and A quick start using Terzo.

Assignments

0. If possible, do this by Friday February 5th. Read the quick start document and execute the examples. The file "list_util.mod" may be found in /cmnusr/local/sml/Terzo/lib/list_util.mod on our local file system.

1. Due Friday February 12th. Prove as many lemmas as possible from lemmas.mod (in this directory), which will be explained in class; check your proofs with checklemmas, and write a lemma or two of your own. Hint: difficult and specialized lemmas are mixed in with easier and more general lemmas; don't feel compelled to do them in order.

2. Due Friday February 19th. Prove some lemmas from basiclem.mod, let.mod, types.mod, and intlist.mod (in this directory), which will be explained in class; check your proofs with checklemmas, and write a lemma or two of your own.

3. Due Friday February 26th. Choose one or more of the following:

  1. Solidify your skill at lemma-hacking by continuing work on assignment 2.
  2. Make "let" versions of the "forall-imp" lemmas.
  3. Define appropriate lemmas for use with "update" and "let_upd".
  4. Convert existing lemmas in types.mod (etc.) for use with new store representation
  5. Define appropriate lemmas to shorten proofs of "all_but_allocated".
  6. Make a lemma generator for all_but_allocated.
You can find source code in /u/appel/proofsem.

4. Due Friday March 5th. Investigate the prover.

Readings

Killer app

George Necula, Proof-Carrying Code, in Twenty-Fourth Annual ACM Symp. on Principles of Prog. Languages, January 1997.

Lambda Prolog and Elf

Amy Felty, lambda Prolog and its Application to Theorem Proving, tutorial slides, 1997.

Dale Miller, lambda Prolog: An Introduction to the Language and its Logic, manuscript, 1998.

Frank Pfenning, Computation and Deduction, course notes, 1997.

Compiling with ...

Andrew Appel, Compiling with Continuations, Cambridge University Press, 1992.

Greg Morrisett, Compiling with Types, PhD Thesis, Carnegie-Mellon University, 1995.

George Necula, Compiling with Proofs, PhD Thesis, Carnegie-Mellon University, 1998.

Zhong Shao, Typed Cross-Module Compilation. Proc. 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP'98), Baltimore, Maryland, pages 141-152, September 1998. ©1998 ACM.

Efficient representation and manipulation of proofs

Gopalan Nadathur, An Explicit Substitution Notation in a lambdaProlog Implementation, December 1997.

Martin Abadi, Luca Cardelli, Pierre-Louis Curien, Jean-Jacques Levy. Explicit Substitutions. Journal of Functional Programming 1(4) 375-416, 1991.

George C. Necula and Peter Lee, Efficient Representation and Validation of Proofs, Proc. 13th Annual Symposium on Logic in Computer Science, 1998.

Zhong Shao, Christopher League, and Stefan Monnier, Implementing Typed Intermediate Languages. Proc. 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP'98), Baltimore, Maryland, pages 313-323, September 1998. ©1998 ACM.

Andrea Asperti and Harry Mairson, Parallel beta reduction is not elementary recursive, 1998 ACM Symposium on the Principles of Programming Languages. Andrea Asperti and Stefano Guerrini, The Optimal Implementation of Functional Programming Languages, Cambridge University Press, 1998.

Soundness of type systems

Andrew Wright and Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, 1994.

Harry Mairson, A constructive logic of multiple subtyping, Proc Twentieth Annual SIGPLAN-SIGACT Symposium on the Principles of Programming Languages, pp. 313-324.

Specification of instruction sets

Norman Ramsey and Mary Fernández. The New Jersey Machine-Code Toolkit. Proceedings of the 1995 USENIX Technical Conference, New Orleans, LA, January 1995, pp 289-302. (Software here)