|
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.
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
- 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 (30%), a midterm exam (30%), and a self-defined final project (40%).
Midterm: 150 points, as 24hour take-home exam, see schedule. Open book. - MORE INFORMATION:
- The course will follow a structure with similarity to S15 instance, which is based on prior instances of this course by John Reynolds and Stephen Brookes, but will also incorporate a number of changes.