Princeton University

Computer Science 441
Programming Languages
Andrew Appel

Fall 2009

General Information       Schedule       Policies

Course Summary

Students will learn the use of the Coq theorem prover for reasoning about programs and programming languages.

Administrative Information

Lectures: MWF 10:00-10:50, Room: 105 CS Building
Labs: Fridays 10:00-10:50 or 11:00-11:50 in Friend 009, in place of some Friday lectures

Note: The determination of whether Friday is to be Lecture or Lab may change as late as Wednesday afternoon; check the Schedule!

Professor: Andrew Appel - 219 CS Building - 258-4627

Teaching Assistants:
C. J. Bell - 215 CS Building - 8-1794
Dr. Lennart Beringer - 217 CS Building - 8-0451
Office Hours: C.J. Bell can often be found in his office in the afternoon and late afternoon; Lennart Beringer between 10 a.m. and 5 p.m.; and Prof. Appel is intermittently available between 9 a.m. and 5 p.m. You can e-mail any one of us for an appointment, or just come over to the 2nd floor of the CS building and try your luck knocking on a door.

Textbooks: Our main text will be Software Foundations by Pierce et al., which is available free online.

We will use the Coq Reference Manual and the Coq Standard Library

We will use the Objective Caml manual.

You may wish to consider purchasing Types and Programming Languages by Pierce (MIT Press 2002); it is an excellent standard textbook and reference on programming-language operational semantics and type systems; it is both broader and deeper than the on-line reference.

Software: We will use the following software.

The Coq theorem prover, version 8.2pl1. This is installed on the computers in Friend 009, 007, and 005. It is free software, and you can install it on your own computer. Windows installation is easy, Macintosh installation is (unfortunately) difficult; see the Coq installation notes.

The Objective Caml dialect of the ML programming language. This is free software. It will (soon) be installed on, it is already installed on, and it will (soon) be in Friend 007 and 005. Or it's easy to install on your own computers. See the Ocaml installation notes.