Lecture — MW 9:00-10:30am — remote via Zoom meeting
Discussion 011 — MW 10:30-11:00pm (same Zoom meeting)
None, but see below for helpful options
autograder.io Homework Code Submission (highest-scoring submission is used)
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. 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.
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.
You will be responsible for:
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.
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.
The grading breakdown is as follows:
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.
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.
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.
You may find the following additional resources helpful:
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.