Princeton University

Computer Science 510
Programming Languages
Andrew Appel

Spring 2019

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: MW 3:00-4:20, Room: Friend 008
Labs: Wednesdays 5-7pm and Friday 1:30-3:30pm in CS 301; Zoe's Thursday office hours 2:30-4:30pm, room CS 216.

Professor: Andrew Appel - CS Building, room 209.
To make an appointment to see me, just ask me after class, or e-mail.

Teaching Assistants: Zoe Paraskevopoulou (room 216) and Santiago Cuellar (room 214).

Use Piazza for homework questions. Better yet: come to Lab, get real-time acoustic 3-D holographic assistance.

Textbooks: Our main texts will be Software Foundations (Volumes 1 and 2 by Pierce et al., Volume 3 by Appel), available free online. (Use the link here, not the Software Foundations home page, to make sure you get the version in sync with this semester's course.) You can download the whole thing as (gzipped tar files) sf.tgz, or (zip files)

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

We will use the Objective Caml manual.

Other required reading (later in the semester):

Dafny tutorial, by Rustan Leino, 2011.

Boolean Satisfiability Solvers: Techniques and Extensions by G. Weissenbacher and S. Malik, in Tools for Analysis and Verification of Software Safety and Security, T. Nipkow, O. Grumberg, B. Hauptmann, G. Kalus, editors, IOS Press, NATO Science for Peace and Security Series, Spring 2012.

Software: We will use the following software.

The Coq theorem prover, version 8.9.0 (download here). It is free software, and you should install it on your own computer.

The OCaml dialect of the ML programming language. This is free software. It is installed on, on, and on OIT cluster computers. Or it's easy to install on your own computers.