
Computer Science 595
Advanced Topics in Software Systems: Automated Theorem Proving
Andrew W. Appel

Fall 2007

General Information
Schedule & detailed syllabus
How to build machinechecked proofs about the safety and correctness of software applications and of programming languages and compilers.
Classes: Monday & Wednesday 1:302:50, Room: 301
Professor: Andrew W. Appel  409 CS Building  2584627
appel@cs.princeton.edu
Prerequisite: (may be taken simultaneously) COS 441 Programming Languages
Syllabus
Theme 1: Practical Logic.
This will be a handson 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 machinechecked proofs.
We will study some recent work by researchers who have constructed
machinechecked proofs about programming models and written readable
papers:
 A constructive denotational semantics for Kahn networks in Coq, by PaulinMohring, 2007. (See also Kahn 1974)
 Engineering formal metatheory, by Aydemir, Chargueraud, Pierce, Pollack, and Weirich, 2007.
 A
very modal model of a modern, major, general type system, by Appel, Mellies, Richards, and Vouillon, 2007.
 Formal certification of a compiler backend, or: programming a compiler with a proof assistant, by Leroy, 2006.

Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves by Rideau, Serpette, and Leroy, 2007.
Theme 3:
Introduction to the programminglanguages
research conducted at Princeton.
 In the style of David August's
research group, how to make a more efficient flow analysis using
ProcedureBoundary Elimination
 In the style of David Walker's research
group, assume that the machine can make mistakes (transient faults),
and use a faulttolerant type system to guarantee that the software
is resilient.
 In the style of Andrew Appel's research group,
see above ("very modal model...").
Readings
The Bertot and Casteran book is on sale at the UStore and on reserve at the Engineering Library.
Coq Documentation is online.
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)