This course is about the formal specification of programming languages, especially in terms of operational semantics and formal type rules. The course objective is to enable students to read, write, and reason about basic formal models of programming languages.

Students will write paper-and-pencil proofs.

The course will cover these these notes.

A light homework assignment will follow most lectures, and it is always due at the beginning of the following class, unless otherwise specified. Homework assignments are posted with the Schedule/Homework Page.

Participants can work on homework in pairs, with the proviso that no pair of students can collaborate on more than 3 homework assignments. Collaborators should submit a single homework solution.

Grades are determined entirely by homework.