Back to Course List

EECS 590: Advanced Programming Languages

Instructor: Westley Weimer

This graduate-level course is designed to acquaint you with the fundamental ideas behind modern programming language design and analysis. Ultimately you should be able to understand current research and apply the techniques here to your own projects.

The course has three broad topics:

  • Semantics
  • Type Systems
  • Research Applications
The first part of this course focuses on the semantics of a variety of programming language constructs. We will study structural operational semantics as a way to formalize the intended execution and implementation of languages. Operational semantics concepts and notation are widely used in modern PL research. We will survey axiomatic semantics, which is useful in developing, as well as verifying, programs. Axiomatic semantics underpin recent research efforts in formal verification and bug finding (e.g., software model checking and proof-carrying code). We will also cover satisfiability modulo theories, automated theorem proving, DPLL(T), and proof checking. We will apply these techniques to imperative, functional and object-oriented languages.

The second part of this course covers the techniques used in the study of type systems for programming languages. We will start our study with the simply-typed lambda calculus. We will also explore more advanced notions, such as types for imperative features and exceptions, parametric polymorphism, existential types for use in abstraction and module systems, and dependent types. Type systems abound in modern PL research and make up the vast majority of formalisms found in papers. Understanding and presenting new type systems is of critical importance when understanding work in this area.

The last part of the course covers special topics drawn from recent research in topics such as concurrency, fault localization, or program repair. In addition to the topics studies in class, students will have the opportunity to consider other related topics of interest in the form of a course project, most often in the form of a survey of recent research about an area of interest.

Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction. Cambridge, MA. MIT Press, 2001.

Full Syllabus and Additional Information
Please see the course web page for more information.