|
|
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 appel@cs.princeton.edu
Teaching Assistants:
C. J. Bell - 215 CS Building - 8-1794
cbell@cs.princeton.edu
Dr. Lennart Beringer - 217 CS Building - 8-0451
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 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.