- Meetings: Monday and Wednesday, 2:00pm to 3:30pm in
1008 EECS.
- Discussion Section: Monday and Wednesday, 3:30pm to 4:00pm in 1008 EECS (right after class, same room)

- Instructor: Wes Weimer.
- Office Hours: Mondays 4:00-4:30, Tuesdays 11:30-Noon, or by appointment (just send email). 4636 Beyster.

- Textbook: Glynn Winskel's
*The Formal Semantics of Programming Languages*.

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 (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:

- Homework assignments. There are six "mathematical" or "formal" problem sets for you to complete by yourself. The homework assignments mostly occur at the beginning of the course. The final assignment has a non-trivial implementation component and involves applying an analysis to real code.
- A Final Project. You will create a final project that explores, extends or experiments with the ideas in the course.
- Reading. While this is not, strictly speaking, a seminar course, there will be a required paper or book chapter assigned after every lecture. Reading quizzes may be employed.

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:

- You do
*not*complete any of the Homework Assignments. - You
*do*participate in class. - You
*do*complete the Final Project. - Your final grade is one letter grade lower than it would be otherwise. That is, if your Final Project and participation would otherwise merit a grade of "A", you would receive a grade of "B" (because you did not complete the homework assignments).

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:

- Hal Abelson, Jerry Sussman, and Julie Sussman's
*Structure and Interpretation of Computer Programs*. The book's full text is available on-line and it is an excellent resource for functional programming and the lambda calculus. - Gordon Plotkin's
*A Structural Approach To Operational Semantics*. The full text is available on-line and provides a great alternate approach to (surprise!) operational semantics. - John Mitchell's
*Foundations for Programming Languages*. - Benjamin Pierce's
*Types and Programming Languages*. - Carl Gunter's
*Semantics of Programming Languages*. - Nielson et al.'s
*Principles of Program Analysis*.