Section is held on Fridays, 4pm-5pm in MD G125. Section attendance is not required. Sections are recorded, and live-streamed.
The following is a list of the sections that were held, and the topic/problems covered.
Videos sections and lectures are available here. You can live stream lectures and sections here.
| Date | Topic |
|---|---|
| Fri 15-Feb | Hoare Logic example. |
| Fri 22-Feb | Concrete vs. abstract syntax; Inductive proof on derivations (IMP big step semantics are deterministic). |
| Fri 1-Mar | The Coq Proof
Assistant. Files: nat.v, imp.v |
| Fri 8-Mar | Review for midterm. Mostly continuations. |
| Fri 29-Mar | Overview of OCaml; parametric polymorphism. |
| Fri 5-Apr | Subtyping; substructural type systems; bounded existentials. |
| Fri 12-Apr | Haskell Programming and monads. Files: monads-section.zip |