Princeton University
Computer Science Department

Computer Science 595
Advanced Topics in Software Systems:
Automated Theorem Proving

Andrew W. Appel

Fall 2007


General Information     Schedule & detailed syllabus

How to build machine-checked proofs about the safety and correctness of software applications and of programming languages and compilers.

Classes: Monday & Wednesday 1:30-2:50, Room: 301
Professor: Andrew W. Appel - 409 CS Building - 258-4627 appel@cs.princeton.edu
Prerequisite: (may be taken simultaneously) COS 441 Programming Languages

Syllabus

Theme 1: Practical Logic. This will be a hands-on course using the Coq theorem prover. I will start with a very simple machine model, and cover, how to specify operational semantics and a type system; how to build machine checked proofs about the operational semantics and type system. Readings for this part include:

Theme 2: Writing and reading about machine-checked proofs. We will study some recent work by researchers who have constructed machine-checked proofs about programming models and written readable papers:

Theme 3: Introduction to the programming-languages research conducted at Princeton.


Readings

The Bertot and Casteran book is on sale at the U-Store and on reserve at the Engineering Library.

Coq Documentation is on-line.

Logic in Computer Science: Modelling and Reasoning About Systems, 2nd Edition, by Huth and Ryan. Cambridge University Press, 2004. (On reserve at the Engineering Library)