EECS 490: Programming Languages

Winter 2022

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 mathematical 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.

Students may also be interested in the following complementary courses:
  • EECS 390 (Programming Paradigms), which focuses more on making effective use of various language features, and less on mathematical first principles and program reasoning. NOTE: EECS 390 is based on material from Amir Kamil's iteration of EECS 490 up through Fall 2019, at which point the courses were split.
  • EECS 483 (Compiler Construction), which goes more in depth on language implementation topics like parsing and low-level optimization that are covered only minimally in this course.


Open in Google Calendar

Day # Lecture Topic Deadline Readings
Wed 5 Jan 1 Course Overview Required: Cornell CS 3110 Notes, Ch. 2
Mon 10 Jan 2 Programming with Mathematical Expressions Required: Cornell CS 3110 Notes, Ch. 3 (except 3.1.3)
Wed 12 Jan 3 Recursive Datatypes and Recursion Schemes Required: Cornell CS 3110 Notes, Ch. 4
Thu 13 Jan
  • Preliminary Survey out
  • A1 out
Mon 17 Jan No Class - MLK Jr. Day
Wed 19 Jan 4 Equational and Inductive Reasoning Required: Princeton COS 326 Notes on Reasoning: Basics, Lists
Mon 24 Jan 5 Syntax
Wed 26 Jan 6 Semantics
Thu 27 Jan
  • Preliminary Survey due
  • A1 due
  • A2 out
Mon 31 Jan 7 Variables and Functions
Wed 2 Feb 8 Types
Thu 3 Feb
  • A2 due
  • A3 out
Mon 7 Feb 9 Products
Wed 9 Feb 10 Recursive Expressions
Thu 10 Feb
  • A3 due
  • A4 out
Mon 14 Feb 11 Sums
Wed 16 Feb 12 Recursive Types
Thu 17 Feb
  • A4 due
  • A5 out
Mon 21 Feb 13 Parametric Polymorphism
Wed 23 Feb 14 Constructive Logic (Proofs are Programs) Optional: Propositions as Types by Philip Wadler
Fri 25 Feb
  • A5 due
Mon 7 Mar - Midterm (during lecture slot, see Piazza)
Wed 9 Mar 15 Dynamic Classification, Gradual Typing, and Typed Holes
  • Mid-Semester Survey out
  • A6 out
Optional: What is Gradual Typing by Jeremy Siek
Mon 14 Mar 16 Imperative Programming I - Side Effects Optional: TAPL Ch. 13
Wed 16 Mar 17 Imperative Programming II - Mutable Data Structures
Thu 17 Mar
  • Mid-Semester Survey due
  • A6 due
  • A7 out
Mon 21 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 23 Mar 19 Imperative Program Verification II
Mon 28 Mar 20 Ownership and Borrowing in Rust I Optional: Rust Book Ch. 4.1-4.2: Understanding Ownership
Wed 30 Mar 21 Ownership and Borrowing in Rust II
Thu 31 Mar
  • A7 due
  • A8 out
Mon 4 Apr 22 Parallelism and Cost Semantics I Optional: PFPL Ch. 37-38
Wed 6 Apr 23 Parallelism and Cost Semantics II
Mon 11 Apr 24 Concurrent Interaction Optional: PFPL Ch. 39
Tue 12 Apr
  • A8 due
  • A9 out
Wed 13 Apr 25 Distributed Computation Optional: PFPL Ch. 40
Mon 18 Apr 26 Macro Systems Optional: Macros - Rust Book
Tue 19 Apr
  • A9 due
  • End-of-semester Survey out
Fri 22 Apr Final Exam (1:30-3:30pm)
Tue 26 Apr
  • End-of-semester Survey due


For technical questions, please use Piazza. For administrative questions, please email the instructional staff collectively at unless you have a specific reason for contacting a staff member individually.
Photo of Cyrus Omar


Photo of David Moon
David Moon


Photo of Johnson He
Johnson He


Photo of Raef Maroof
Raef Maroof


Photo of Tonia Li
Tonia Li


Photo of Nicholas Spihlman
Nicholas Spihlman