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)
- 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.