2 Topics
The primary text for the course is:
Benjamin C. Pierce: Types and Programming Languages
Not all of the book will be covered, and other material is
used as well, but this book will be necessary to have.
The course aims to deepen understanding on the concepts and features
of programming languages, and provide means to (formally) reason about languages
and language features, to the extent to become able to appreciate current research
and developments in the area of programming languages.
Programming languages are a huge area. Consequently, the course tries to focus on
fundamental mechanism rather than broadness. Not everything can be covered:
the text focuses on static typing, type systems etc.,
which will comprise the main body of this course as well.
We start from the lambda calculus as the simplest model of a programming
language, and gradually extend it with language features.
The basics that are covered include
-
Specifying semantics of programming languages
- Necessary proof techniques for programming language research
- Lambda calculus
- Specifying type systems
- Formal study of properties of type systems and languages (such
as type safety)
Equipped with this basic skill set, we'll study more ambitious
language constructs, such as:
-
Subtyping
- Polymorphism and generics
- Constrained generics (bounded quantification)
- Recent advances/questions in programming languages/type systems
A likely class project will be an in-depth study of an interesting topic
covered by the last bullet above.