
Computer Science 441


Students will learn the use of the Coq theorem prover for reasoning about programs and programming languages.
Professor: Andrew Appel  219 CS Building  2584627 appel@cs.princeton.edu
Teaching Assistants:
C. J. Bell  215 CS Building  81794
cbell@cs.princeton.edu
Dr. Lennart Beringer  217 CS Building  80451
eberinge@cs.princeton.edu
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 email 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.
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 programminglanguage operational semantics and type systems; it is both broader and deeper than the online reference.
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 hats.princeton.edu, it is already installed on penguins.cs.princeton.edu, 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.