| Date | Topic | PFPL Chapters | Homework |
|---|---|---|---|
| Jan 14 | Introduction: What is a programming language? | 1-3 | Assignment 0 Out |
| Jan 15 | Rule Induction (handout) | ||
| Jan 16 | Rule induction, Binding, Substitution | 4-5 | |
| Jan 21 | Dynamics, Statics, and Safety | 4-7 | Assignment 0 Due, Assignment 1 Out |
| Jan 22 | Abstract Syntax and De Bruijn Indices (handout) | ||
| Jan 23 | Functions (Guest Speaker: Frank Pfenning) | 8 | Solution 0 Out |
| Jan 28 | Gödel's T and PCF (notes) | 10 | |
| Jan 29 | Substitution Lemma (handout) | ||
| Jan 30 | Definability and undefinability | 9 | |
| Feb 4 | Products and Sums | 11-12 | Assignment 1 Due, Assignment 2 Out |
| Feb 5 | Products, Sums, and Pattern Matching (handout) | ||
| Feb 6 | Recursive Types | 16 | Solution 1 Out |
| Feb 11 | Objects and Dynamic Dispatch | 25 | |
| Feb 12 | Proof Techniques (handout) | ||
| Feb 13 | Dynamic Languages | 18 | |
| Feb 18 | Dynamic Languages as Typed Languages | 19 | Assignment 2 Due, Assignment 3 Out |
| Feb 19 | Dynamic and Hybrid Typing (handout) | ||
| Feb 20 | Church's λ-Calculus | 17 | |
| Feb 25 | Modernized Algol | 36 | |
| Feb 26 | Dynamic Typing and Refinements (handout) | ||
| Feb 27 | Scoped Assignables | 36 | |
| Mar 4 | Assignable References | 37 | Assigment 3 Due |
| Mar 5 | |||
| Mar 6 | Midterm Exam | Solutions | |
| Spring break woooooo… | |||
| Mar 18 | System F and Polymorphism | 20 | |
| Mar 19 | Polymorphism (handout) | ||
| Mar 20 | Representation Independence (notes) | 21 | |
| Mar 25 | Evaluation Dynamics | 7 | Assignment 4 Out |
| Mar 26 | Cost Dynamics and Parallelism (handout) | ||
| Mar 27 | Nested Data Parallelism (notes) | 40 | |
| Apr 1 | Control Stacks (notes) | 28 | |
| Apr 2 | Stacks (handout) | ||
| Apr 3 | Brent's Theorem (notes) | 40 | |
| Apr 8 | Free Assignables, Monads | 37 | Assignment 4 Due, Assignment 5 Out |
| Apr 9 | |||
| Apr 10 | (Carnival: no class) | ||
| Apr 15 | Futures and Speculations (notes) | 41 | |
| Apr 16 | Call by Need (handout) | ||
| Apr 17 | Communication in the π-calculus | 42 | |
| Apr 22 | Concurent Algol | 43 | Assignment 5 Due, Asignment 6 Out |
| Apr 23 | Concurent Algol (handout) | ||
| Apr 24 | Proofs as Programs | 31 | |
| Apr 29 | Judgments as Types | ||
| Apr 30 | |||
| May 1 | Dependently Typed Programming | Assignment 6 Due | |
| Final exams noooooo… | |||
| May 6 | 15-312 Final exam: May 6, 1pm-4pm (BH 136A) | ||
| Summer vacation ahhhhhh… | |||