Lectures and Details (Winter 2020)

Overview

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. A good additional reference for this part of the course is 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.

Course Prerequisites

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, via 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.

Assignment Overview

You will be responsible for:

• Homework assignments. There are six "mathematical" or "formal" problem sets. The final assignment has a non-trivial implementation component and involves applying an analysis to real code.
• Reading Quizzes. While this is not, strictly speaking, a seminar course, there will be a required paper or book chapter assigned for every lecture. Reading quizzes will be employed.
  • Reading quizzes will generally be deployed via gradescope. Reading quizzes will generally become available the morning over the day the reading is due. You will generally have a large window of time (e.g., 48 hours) during which you can begin the reading quiz. Once you begin the reading quiz, you will generally have a smaller amount of time (e.g., 5 minutes) to complete the quiz. To put this another way, you can choose any 5 minute window within 48 hours to take the quiz. In practice we typically allow extra time (e.g., you may use 10 minutes instead of 5) as an accommodation for remote education (e.g., network issues) or SSD concerns. As a result of these large grace periods it will be difficult for us to make any further accommodations for students who miss the quizzes.
• Participation and Peer Review. We will track participation during remote (Zoom) lectures. In addition, because one of the class goals is to assess uses of the formalisms in this research area, we will walk through and peer grade homework submissions during the discussion sections. For each assignment, you are responsible for submitting an assessment of a peer's submission.

A deliverable turned in h hours late has its point value reduced by (h * 2)%. We follow the Rackham Academic and Professional Integrity Policy. We cannot accept an assignment submission after the corresponding answer key has been discussed in class.

Remote Education and Accommodations

Students who are more than one time zone away may not be able to attend lectures and demonstrate participation in the usual manner. Students with U-M SSD forms should present those as quickly as possible. While there are no exams or similar timed assignments, we will work to find fair ways to support students completing the material.

Grading and Examinations

The grading breakdown is as follows:

Regrade, Late Add and Makeup Policy

Regrade requests for exams, assignments, or written assignments must be received within one week of you receiving your score. All regrade requests should be made via gradescope. When we regrade an assignment we will look over it very carefully for correctness: it is possible that after a regrade you will end up with fewer points than before the regrade. Regrades should be treated with caution and used only when the graders have made a clear mistake evaluating your work.

If you miss an assignment deadline or in-class activity, we can be very lenient about extensions or makeups but only if you provide documentation. For example, for death or bereavement, a copy of the obituary or funeral program suffices; for illness or injury, any sort of doctor's note suffices. This policy follows that of other professors in the department. You may email the TA with supporting documentation.

All course materials submitted for a grade must be turned in by midnight on the last date listed on the course syllabus.

Students who add the course late are still responsible for all assignments at the normal due date. If you are interested in taking the course and are on the waiting list, you should complete all assignments as usual.

Waiting List

There are currently no plans to increase enrollment beyond the course's listed capacity. However, students often drop courses after the first few lectures or near the first assignment.

All students on the waiting list will be given full access to the course forum, lectures, grading submissions, and discussion activities.

Student Mental Health

Students often experience strained relationships, increased anxiety, alcohol or drug problems, feeling down, difficulty concentrating, family issues, or a lack of motivation. Student mental health concerns are quite common but we don't always talk about them. The University of Michigan is committed to advancing the mental health and well-being of its students. If you or someone you know is feeling overwhelmed, depressed, or in need of support, confidential mental health services are available on campus.

Optional References

You may find the following additional resources helpful:

• Glynn Winskel's The Formal Semantics of Programming Languages. This book is often used in graduate programming languages courses.
• 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.

Research

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 or teaching assistant to do so after final grades have been issued. This has no impact on your grade in any manner.

Students interested in considering undergraduate research should make an appointment to talk about it. I am happy to discuss independent study projects, senior projects, paid research work over the summer, research work for credit, and graduate school.