CSCI-B522: Programming Language Foundations
Spring 2026
This is a graduate course on the theoretical foundations of programming languages. We will learn fundamental techniques for formally defining programming languages and for proving properties of those languages and the programs written in them. Topics will include abstract syntax with binding, operational semantics, type safety, logical relations, and observational equivalence.
By the end of the course, students will be able to:
- formally define a variety of programming languages by their statics (type systems) and dynamics (operational semantics),
- prove theorems relating a language's statics and dynamics,
- formally define and reason about equivalence of program fragments, and
- appreciate the importance of compositionality and abstraction in the design of programming languages.