|
|
Computer Science 510
|
|
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.
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.
We will use the Coq 8.3 Reference Manual and the Coq 8.3 Standard Library
We will use the Objective Caml manual.
Other required reading (later in the semester):
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.3pl5. (Careful: not version 8.4) 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.
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.