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

15-812 Programming Language Semantics (Spring 2015)

Instructor:	André Platzer (office: T 1:00-2:00, GHC 9103)
Teaching Assistant:	Kristina Sojakova (ksojakov@andrew) (office: M 2:00-3:00, GHC 7121)
Units:	12
Semester:	Spring 2015
Time:	TR 10:30-11: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.

Schedule

DESCRIPTION:

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.

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, as well as ways of integrating these paradigms into more general languages. The range of possible topics includes:

semantics of programming languages (denotational and operational semantics)
program specification and proof (Hoare logic, dynamic logic, weakest preconditions, and separation logic)
concurrent programming (shared-variable and message-passing approaches)
functional programing (continuations and lazy evaluation)
interactive and game programming (multi-agent programs)
type systems (subtyping, polymorphism, and modularization)

In exploring these topics, we will use a variety of fundamental concepts and techniques, such as compositional semantics, binding structure, domains, transition systems, and proof rules. Precedence in this course will always be given to identifying and understanding the core principles rather than an exhaustive coverage of all aspects of programming languages.

PREREQUISITES:

There are no specific prerequisites, but the course expects you to have or acquire some background in programming languages and basic mathematics.

METHOD OF EVALUATION:

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, Thu 04/02 as 24hour take-home exam. Open book.

MORE INFORMATION:

The course will follow a structure with similarity to prior instances of this course by John Reynolds and Stephen Brookes, but will also incorporate a number of changes.