Sections are held:
- Coq Section: Wednesday, 11:30am– 12:30pm
- Weekly Section: Friday, 11am–12pm
Section attendance is not required. You can go to whichever section(s) you want. One of the sections will be recorded.
Some sections are recorded. Videos of the lecture and section are available on Canvas / Extension Class Meetings.
Extension school students: you can join zoom for section (and participate remotely) on Canvas / Extension Class Meetings. 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 | Operational Semantics (small-step, large-step); Induction | PDF Solutions |
| 4 | IMP; Denotational Semantics | PDF Solutions |
| 5 | Lambda calculus basics; Lambda calculus encodings and Recursion | PDF Solutions |
| 6 | Definitional translations; References and continuations | PDF Solutions |
| 7 | Simply-typed lambda calculus; More types | PDF Solutions |
| 8 | Parametric Polymorphism; Records and Subtyping; Curry-Howard Isomorphism; Existential Types | PDF Solutions |
| 9 | Type Inference | PDF Solutions |
| 10 | Sub-structural type systems; Algebraic structures (Haskell Code) | PDF Solutions |
| 11 | Environment Semantics; Axiomatic Semantics; Dependent Types | PDF Solutions |
| 12 | Logic Programming; Dynamic Types; Probabilisitc Programming | PDF Solutions |