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 - 258-4627 firstname.lastname@example.org
C. J. Bell - 215 CS Building - 8-1794 email@example.com
Dr. Lennart Beringer - 217 CS Building - 8-0451 firstname.lastname@example.org
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.
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.
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.