
Computer Science 510


Summary: A handson 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.
Professor: Andrew Appel  CS Building, room 209.
appel@cs.princeton.edu
To make an appointment to see me, just ask me after class, or email.
Teaching Assistant: Josh Cohen  CS Building, room 244
Use Ed for homework questions. You can also come to Lab hours.
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 tutorials, by Rustan Leino and others, 20112023.
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.
The Coq theorem prover, version 8.16.1.
Installation instructions here with quick summary as follows:
Installation: Coq Platform 2022.09.1 Use one of the "Recommended binary installers" for your own computer (Windows, macOS, or Linux). I recommend the "full level" install PLUS the following two optional packages: CompCert (coqcompcert.3.11) and VST (coqvst.2.11.1).
The OCaml
dialect of the ML programming language.
Very possibly the Coq Platform installation (see above) will install ocaml for you as well.