Instructor
comar@umich.edu
Winter 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 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 | |
---|---|---|---|---|---|
Wed 4 Jan | 1 | Course Overview | |||
Mon 9 Jan | 2 | Programming with Mathematical Expressions |
|
Optional: Cornell CS 3110 Notes, Ch. 2-3 (except 3.1.3) | |
Wed 11 Jan | 3 | Recursive Datatypes and Recursion Schemes | Optional: Cornell CS 3110 Notes, Ch. 4 | ||
Mon 16 Jan | No Lecture (MLK Jr. Day) | ||||
Wed 18 Jan | 4 | Equational and Inductive Reasoning | Optional: Princeton COS 326 Notes on Reasoning: Basics, Lists | ||
Sat 21 Jan |
|
||||
Mon 23 Jan | 5 | Syntax | |||
Wed 25 Jan | 6 | Semantics |
|
||
Fri 27 Jan |
|
||||
Sat 28 Jan |
|
||||
Mon 30 Jan | 7 | Variables and Types | |||
Wed 1 Feb | 8 | Functions (the Lambda Calculus) | |||
Thu 2 Feb |
|
||||
Mon 6 Feb | 9 | Products |
|
||
Wed 8 Feb | 10 | Sums | |||
Sat 11 Feb |
|
||||
Mon 13 Feb | 11 | Recursive Expressions | |||
Wed 15 Feb | 12 | Recursive Types | |||
Fri 17 Feb |
|
||||
Mon 20 Feb | 13 | Universal Types (Parametric Polymorphism) | |||
Wed 22 Feb | 14 | Constructive Logic (Proofs are Programs) | Optional: Propositions as Types by Philip Wadler | ||
Fri 24 Feb |
|
||||
Sat 25 Feb - Sun 5 Mar | Break | ||||
Mon 6 Mar | 15 | Dynamic Classification, Gradual Typing, and Typed Holes | Optional: What is Gradual Typing by Jeremy Siek | ||
Wed 8 Mar | Midterm Exam (during lecture) | ||||
Thu 9 Mar |
|
||||
Mon 13 Mar | 16 | Imperative Programming I - Side Effects | Optional: TAPL Ch. 13 | ||
Wed 15 Mar | 17 | Imperative Programming II - Mutable Data Structures | |||
Thu 16 Mar |
|
||||
Mon 20 Mar | 18 | Imperative Program Verification I | Optional: CMU
17-654: Hoare Logic:
Proving Programs Correct Optional: Washington CSE 331: Reasoning About Code (Hoare Logic) |
||
Wed 22 Mar | 19 | Imperative Program Verification II | |||
Mon 27 Mar | 20 | Ownership and Borrowing in Rust I | Optional: Rust Book Ch. 4.1-4.2: Understanding Ownership | ||
Wed 29 Mar | 21 | Ownership and Borrowing in Rust II | |||
Thu 30 Mar |
|
||||
Mon 3 Apr | 22 | Parallelism and Cost Semantics I | Optional: PFPL Ch. 37-38 | ||
Wed 5 Apr | 23 | Parallelism and Cost Semantics II | |||
Mon 10 Apr | 24 | Concurrent Interaction | Optional: PFPL Ch. 39 | ||
Tue 11 Apr |
|
||||
Wed 12 Apr | 25 | Distributed Computation and Module Systems | Optional: PFPL Ch. 40 | ||
Mon 17 Apr | 26 | Special Topic: Macro Systems |
|
||
Tue 18 Apr |
|
||||
Mon 24 Apr | Final Exam (1:30-3:30pm) (Location: 1013 DOW) | ||||
Tue 25 Apr |
|
GSI
dmoo@umich.edu
IA
hejohns@umich.edu
IA
zwgold@umich.edu
Grader
hailunzh@umich.edu
Grader
rajvarun@umich.edu
Grader
ypei@umich.edu