CSE 505: Programming Languages


We'll study techniques for thinking crisply about programming languages, write some fascinating programs, and discuss various design tradeoffs. We will roughly follow Dan Grossman's traditional 505 material using the Lean proof assistant.

Meeting Mon, Wed 9:30 ARC G070
Instructor Zach Tatlock (ztatlock@cs)
Friday 10:30 - 11:30 CSE 546
Instructor Leonardo De Moura (leonardo@microsoft.com)
TA Jared Roesch (jroesch@cs)
Wednesday 3:00pm - 4:00pm CSE 2nd Floor breakout
Discussion Piazza,
Scores 505 Gradebook


Wed, Sep 27
Mon, Oct 2
Wed, Oct 4
Mon, Oct 9
Wed, Oct 11
Mon, Oct 16
Wed, Oct 18
Mon, Nov 6
Wed, Nov 8
Mon, Nov 13
Wed, Nov 15
Mon, Nov 20
Wed, Nov 22
Mon, Nov 27
Wed, Nov 29
Wed, Dec 6
17   Parametric Polymorphism   [materials]


We'll read and discuss a handful of papers this quarter. Most of the readings are relatively non-technical; they're intended to foster discussion and debate. By noon the day before each discussion, please submit a short review. Your review should have three small paragraphs: (1) a high-level summary of the paper and a concise recap of its main take-away; (2) a description of what you most valued learning from the paper and what the paper's greatest strengths are; and (3) a discussion of what you disagreed with or felt could be improved to make the paper stronger.

Please submit your reviews in plain text format , in a single file, including only ASCII characters (no Unicode please), as NETID.txt where NETID is your UW Net ID, via the 505 Dropbox. (Please note, this means you should NOT submit a PDF!)

Mon, Oct 9
Mon, Oct 30
Mon, Nov 20
Social Processes and Proofs of Theorems and Programs


Please work on your homeworks with a partner. It should be more fun and help you meet folks in the department you may not have otherwise gotten a chance to work with. To find a partner who is not in your lab, try the Piazza partner search. Also, make sure to work with a different partner for each homework. Only one member of each team should submit a solution. Please clearly indicate both team members in a comment at the top of your submission. Happy hacking :)

Submit homeworks via the 505 Dropbox. If you absolutely must, you can submit up to 2 days late, but the policy is to subtract 10% per day.

Homework 0 is due at noon on September 29.

Homework 1 is due at noon on October 17.

Homework 2 is due at noon on November 14.

Homework 3 is due at noon on December 14.


Unlike homeworks, exams should be entirely your own work. Please submit your exam via the 505 Dropbox.


You can always get help on Piazza, but nothing beats a genuine face-to-face meeting.

If you'd like to interact with a real person please come to Zach's office hours (Friday at 10:30 CSE 546), Jared's office hours (Wednesday at 3pm CSE 218, 2nd Floor Breakout). Because schedules are hectic, some times and locations may change throughout the quarter, so please reach out if you're stuck!


Setting up Lean

We have built a new set of scripts for managing your Lean installation, you can read about installation and use here.


You can read the official documentation page for Lean, specifically An Introduction to Lean and Theorem Proving in Lean. There is also an in progress reference manual for the Lean programming language.

The classic 505 materials and Types and Programming Languages textbook are also excellent for learning all the material we'll cover in class and more, but from a traditional pen-and-paper perspective.