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:
The first part of this course focuses on the semantics of a variety of programming language constructs (e.g., "what does a while loop really mean?" — this is actually much more exciting than it sounds). 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., proof-carrying code and SLAM). 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. We will make use of the presentation of these topics in Glynn Winskel's The Formal Semantics of Programming 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 the "Greek letters" found in papers. Understanding and presenting new type systems is of critical importance when doing work in this area. A good additional reference for this part of the course is John Mitchell's Foundations for Programming Languages.
The last part of the course covers special topics drawn from recent research in topics such as concurrency, fault localization, or program repair. The list of lecture topics also serves as summary of key course concepts.
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 on a topic of interest.
The prerequisites for this course are programming and mathematical experience. The ideal programming experience is an undergraduate compilers course as well as practical exposure to several different programming languages, such as C, ML, LISP and Java. The ideal mathematical experience is a knowledge of mathematical logic and the ability to construct rigorous proofs (in particular by structural induction). These prerequisites are not strict. However, your desire to be exposed to this material is very important. In the past a small number of undergraduates have been able to complete the course.
Notably, an undergraduate programming languages course is not required. Students without the relevant undergraduate background should be prepared to put additional time into this course and seek out help and additional resources on their own.
You will be responsible for:
An assignment turned in d days late has its point value reduced by (d * 10)%. We follow the Rackham Academic and Professional Integrity Policy.
In response to student demand, you have the option (this is not required) of committing to the following grading contract:
This grading contract may be appropriate for students pursuing a self-funded coursework-based professional Master's degree, for example. Such students may not be interested in pursuing a research career and may not have the time to give full attention to all aspects of this course.
To opt-in to this alternate grading contract, follow the instructions in the first homework assignment.
Your class work might be used for research purposes. For example, we may use anonymized student assignments to design algorithms or build tools to help programmers. Any student who wishes to opt out can contact the instructor to do so after final grades have been issued. This has no impact on your grade in any manner.
Students interested in considering graduate or undergraduate research should make an appointment with me to talk about it. I am happy to discuss graduate advising, independent study projects, senior theses, paid research work over the summer, research work for credit, and graduate school applications.
You may find the following additional resources helpful: