Sections are held:
- Tuesdays 3pm-4:15pm in Northwest B105
- Fridays 12pm-1:15pm in Northwest B150
Section attendance is not required. You can go to whichever section(s) you want. One of the sections will be recorded.
Tuesday sections are recorded. Videos of the lecture and section are available here.
Extension school students: you can join zoom for section (and participate remotely) at https://harvard-dce.zoom.us/j/490714503?status=success. If you do want to join remotely, please email the course staff in advance, so they can make sure they are prepared.
The following is a list of the sections that were held, and the topic/problems covered. Practice problems will typically be released on Fridays.
| Week | Topic | Practice problems |
|---|---|---|
| 3 | Induction; Small-step operational semantics; Large-step operational semantics | PDF Solutions |
| 4 | IMP; Denotational semantics | PDF Solutions |
| 5 | Lambda calculus basics; Lambda calculus encodings | PDF Solutions |
| 6 | Definitional translations; References, continuations | PDF Solutions |
| 7 | Simply-typed lambda calculus; More types | PDF Solutions |
| 8 | Type inference | PDF Solutions |
| 9 | Parameteric polymorphism, records and subtyping, Curry-Howard, existential types | PDF Solutions |
| 10 | Sub-structural type systems; Algebraic structures (Haskell code) | PDF Solutions |
| 11 | Environment Semantics; Axiomatic semantics; Dependent Types (Haskell code) | PDF Solutions |
| 12 | Proof tools; Ethics and specifications | |
| 13 | Logic Programming (Prolog code, Datalog code); Dynamic Types and Contracts | PDF Solutions |
| 14 | Review |