15-812: Programming Language Semantics (Sp'18)

15-812 Programming Language Semantics (Spring 2018)
Instructor: André Platzer
(office: TBD)
Units: 12
Semester: Spring 2018
Time: TR 1:30-2:50
Place: GHC 4303
This course counts as a Programming Languages star course in the Computer Science curriculum. It is listed in the Computer Science Department as 15-812 at Carnegie Mellon University.

Programs are used everywhere, often to reach or influence important decisions. That is why we need strong guarantees about what a program computes, so that we can trust its result. Guarantees begin with program semantics, which defines in mathematically precise terms what a program will do if executed, and lead to rigorous reasoning techniques for understanding the effect of a program.

This course will place an emphasis on what students need to know to justify correctness of their understanding or analysis or compilation of programs. It will avoid technicalities whenever possible without losing sight of the crucial phenomena.

In this course, we survey the theory behind the design, description, and implementation of programming languages, and methods for specifying and verifying program behavior. The primary purpose of this course is to develop an understanding of how programming languages can be given an unambiguous meaning and how programs in that language can be analyzed to identify if they do what they are supposed to. We will learn how to characterize programming languages syntactically, semantically, and axiomatically in ways that align their semantics and rigorous reasoning principles in perfect unison.

Both imperative and functional programming languages are covered in this course. The range of possible topics includes:

  • semantics of programming languages (denotational and operational semantics)
  • program specification and proof (dynamic logic and separation logic)
  • interactive and game programming (multi-agent programs)
  • functional programing (continuations and lazy evaluation)
  • concurrent programming (shared-variable and message-passing approaches)
  • correct compilation and interpretation
In exploring these topics, we will use a variety of fundamental concepts and techniques, such as compositional semantics, static semantics, transition systems, and proof rules. Precedence in this course will always be given to identifying and understanding the most impactful core principles rather than an exhaustive coverage of all aspects of programming languages.

There are no specific prerequisites, but the course expects you to have or acquire some background in programming languages and basic mathematics.
Grading will be based on a set of homework assignments (41%), a midterm exam (25%), and a self-defined final project (33%).
Midterm: 150 points, TBD as 24hour take-home exam. Open book.
The course will follow a structure with similarity to prior instance based on prior instances of this course by John Reynolds and Stephen Brookes, but will also incorporate a number of changes.