Department
Princeton University

Computer Science 441
Programming Languages
Andrew Appel

Fall 2010

General Information       Schedule       Policies
Summary: A hands-on introduction to the use of formal methods for reasoning about software, and for specifying and reasoning about programming languages. Students will use an interactive proof assistant to learn about logic and its applications to proofs of program correctness, to operational and axiomatic semantics of programming languages, and to type systems. Also, an introduction to functional programming languages.

Administrative Information

Lectures: MWF 10:00-10:50, Room: 102 Computer Science
Labs: Fridays 10:00-10:50 or 11:00-11:50 in Friend 009, in place of some Friday lectures
Sunday Labs: Friend 009 will be staffed with a teaching assistant Sundays 5-7 p.m. and 8:30-10:30 p.m.
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 appel@cs.princeton.edu
To make an appointment to see me, just ask me after class or call/email Nicole, 8-4624.

Teaching Assistants:
Michael Ty (Laboratory assistant for help in Friend 009 on Friday mornings and Sunday evenings; and feel free to e-mail him for an appointment for extra assistance with the homeworks.)
C. J. Bell (Grader, and you can see him for general questions and assistance with the coursework)

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 is installed on hats.princeton.edu, on penguins.cs.princeton.edu, and in Friend 009/007/005. Or it's easy to install on your own computers. See the Ocaml installation notes.