Instructor
comar@umich.edu
Fall 2024
Programming languages are rich mathematical structures and powerful user interfaces. This course covers the design and use of modern programming languages. We will build up systematically from formal first principles while considering human factors in language design, language prototyping, and techniques for reasoning precisely about program behavior throughout the course.
The goal is to change the way you think about programming and programming language design in ways that will remain relevant across the many technology hype cycles that you will encounter over the course of your careers.
Day | # | Lecture Topic | Deadline | Readings |
---|---|---|---|---|
Tue 27 Aug | 1 | Course Overview | Required: EECS 490 Syllabus | |
Thu 29 Aug | 2 | Programming with Mathematical Expressions |
|
Optional: Cornell CS 3110 Notes, Ch. 2-3 (except 3.1.3) |
Tue 3 Sep | 3 | Recursive Datatypes and Recursion Schemes |
|
Optional: Cornell CS 3110 Notes, Ch. 4 |
Thu 5 Sep | 4 | Equational and Inductive Reasoning | Optional: Princeton COS 326 Notes on Reasoning: Basics, Lists | |
Tue 10 Sep | 5 | Syntax | ||
Thu 12 Sep | 6 | Semantics | ||
Fri 13 Sep |
|
|||
Tue 17 Sep | 7 | Variables and Types | ||
Thu 19 Sep | 8 | Functions (the Lambda Calculus) | ||
Fri 20 Sep |
|
|||
Tue 24 Sep | 9 | Products and Isomorphisms | ||
Thu 26 Sep | 10 | Sums | ||
Fri 27 Sep |
|
|||
Tue 1 Oct | 11 | Recursive Expressions | ||
Thu 3 Oct | 12 | Recursive Types | ||
Fri 4 Oct |
|
|||
Tue 8 Oct | 13 | Universal Types (Parametric Polymorphism) | ||
Thu 10 Oct | 14 | Constructive Logic (Proofs are Programs) | Optional: Propositions as Types by Philip Wadler | |
Fri 11 Oct |
|
|||
Tue 15 Oct | No Lecture - Fall Study Break | |||
Thu 17 Oct | Midterm Exam (in class) | |||
Tue 22 Oct | 15 | Dynamic Classification, Gradual Typing, and Typed Holes |
|
Optional: What is Gradual Typing by Jeremy Siek |
Thu 24 Oct | 16 | Imperative Programming I - Side Effects | Optional: TAPL Ch. 13 | |
Fri 25 Oct |
|
|||
Tue 29 Oct | 17 | Imperative Programming II - Mutable Data Structures 😱 | ||
Thu 31 Oct | 18 | Imperative Program Analysis I | Optional: CMU
17-654: Hoare Logic:
Proving Programs Correct Optional: Washington CSE 331: Reasoning About Code (Hoare Logic) |
|
Fri 1 Nov |
|
|||
Tue 5 Nov | 19 | Imperative Program Analysis II | ||
Thu 7 Nov | 20 | Memory Management + Ownership in Rust | Optional: Rust Book Ch. 4.1-4.2: Understanding Ownership | |
Tue 12 Nov | 21 | Borrowing in Rust | ||
Thu 14 Nov | 22 | Parallelism and Cost Semantics I | Optional: PFPL Ch. 37-38 | |
Fri 15 Nov |
|
|||
Tue 19 Nov | 23 | Parallelism and Cost Semantics II | ||
Thu 21 Nov | 24 | Concurrent Interaction | Optional: PFPL Ch. 39 | |
Fri 22 Nov |
|
|||
Tue 26 Nov | No Lecture - Happy Thanksgiving! | |||
Thu 28 Nov | No Lecture - Happy Thanksgiving! | |||
Tue 3 Dec | 25 | Distributed Computation and Module Systems | Optional: PFPL Ch. 40 | |
Thu 5 Dec | 26 | Special Topic: TBA | ||
Fri 6 Dec |
|
|||
Fri 13 Dec |
|
|||
Wed 18 Dec | Final Exam (10:30am-12:30pm) (Location: TBD) |
GSI
gregtc@umich.edu
Grader
lmulcahy@umich.edu