Instructor
comar@umich.edu
Fall 2023
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 29 Aug | 1 | Course Overview | ||
Thu 31 Aug | 2 | Programming with Mathematical Expressions |
|
Optional: Cornell CS 3110 Notes, Ch. 2-3 (except 3.1.3) |
Tue 5 Sep | 3 | Recursive Datatypes and Recursion Schemes | Optional: Cornell CS 3110 Notes, Ch. 4 | |
Thu 7 Sep | 4 | Equational and Inductive Reasoning | Optional: Princeton COS 326 Notes on Reasoning: Basics, Lists | |
Fri 8 Sep |
|
|||
Tue 12 Sep | 5 | Syntax | ||
Thu 14 Sep | 6 | Semantics | ||
Fri 15 Sep |
|
|||
Tue 19 Sep | 7 | Variables and Types | ||
Thu 21 Sep | 8 | Functions (the Lambda Calculus) | ||
Fri 22 Sep |
|
|||
Tue 26 Sep | 9 | Products and Isomorphisms | ||
Thu 28 Sep | 10 | Sums | ||
Fri 29 Sep |
|
|||
Tues 3 Oct | 11 | Recursive Expressions | ||
Thu 5 Oct | 12 | Recursive Types | ||
Fri 6 Oct |
|
|||
Tue 10 Oct | 13 | Universal Types (Parametric Polymorphism) | ||
Thu 12 Oct | 14 | Constructive Logic (Proofs are Programs) | Optional: Propositions as Types by Philip Wadler | |
Fri 13 Oct |
|
|||
Tue 17 Oct | No Lecture (Fall Study Break) | |||
Thu 19 Oct | Midterm Exam (in class) | |||
Tue 24 Oct | 15 | Dynamic Classification, Gradual Typing, and Typed Holes |
|
Optional: What is Gradual Typing by Jeremy Siek |
Thu 26 Oct | 16 | Imperative Programming I - Side Effects | Optional: TAPL Ch. 13 | |
Fri 27 Oct |
|
|||
Tue 31 Oct | 17 | Imperative Programming II - Mutable Data Structures 😱 |
|
|
Thu 2 Nov | 18 | Imperative Program Verification I | Optional: CMU
17-654: Hoare Logic:
Proving Programs Correct Optional: Washington CSE 331: Reasoning About Code (Hoare Logic) |
|
Fri 3 Nov |
|
|||
Tue 7 Nov | 19 | Imperative Program Verification II | ||
Thu 9 Nov | 20 | Ownership and Borrowing in Rust I | Optional: Rust Book Ch. 4.1-4.2: Understanding Ownership | |
Tue 14 Nov | 21 | Ownership and Borrowing in Rust II | ||
Thu 16 Nov | 22 | Parallelism and Cost Semantics I | Optional: PFPL Ch. 37-38 | |
Fri 17 Nov |
|
|||
Tue 21 Nov | 23 | Parallelism and Cost Semantics II | ||
Thu 23 Nov | No Lecture (Thanksgiving) | |||
Tue 28 Nov | 24 | Concurrent Interaction | Optional: PFPL Ch. 39 | |
Thu 30 Nov | 25 | Distributed Computation and Module Systems | Optional: PFPL Ch. 40 | |
Fri 1 Dec |
|
|||
Tue 5 Dec | 26 | Special Topic: TBA |
|
|
Fri 8 Dec |
|
|||
Thu 14 Dec | Final Exam (10:30am-12:30pm) (Location: TBD) | |||
Fri 15 Dec |
|
GSI
blinnand@umich.edu
IA
zzhaoe@umich.edu
Grader
tingtind@umich.edu
Grader
weixiao@umich.edu