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 398 (Programming Paradigms), which focuses more on making effective use of various language features, and less on mathematical first principles and program reasoning.
  • 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 Recursive Expressions + Products
Wed 9 Feb 10 Sums
Thu 10 Feb
  • A3 due
  • A4 out
Mon 14 Feb 11 Recursive Types
Wed 16 Feb 12 Polymorphism
Thu 17 Feb
  • A4 due
  • A5 out
Mon 21 Feb 13 Constructive Logic (Proofs are Programs) Optional: Propositions as Types by Philip Wadler
Wed 23 Feb 14 Dynamic Classification, Gradual Typing, and Typed Holes Optional: What is Gradual Typing by Jeremy Siek
Thu 24 Feb
  • A5 due
  • A6 out
Mon 7 Mar - Midterm (during lecture slot, see Piazza)
Wed 9 Mar 15 Imperative Programming I - Side Effects
  • Mid-Semester Survey out
Optional: TAPL Ch. 13
Mon 14 Mar 16 Imperative Programming II - Mutable Data Structures
  • A6 due
  • A7 out
Wed 16 Mar 17 Encapsulated Commands (e.g. Haskell's IO types) Optional: Introduction to IO (Haskell Wiki)
Thu 17 Mar
  • Mid-Semester Survey due
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