Sections are held:

- Tuesdays 2-3pm, led by Anastasiya and including Coq
- Wednesdays 7-8pm, led by Amanda and Jack

Section attendance is not required. You can go to whichever section(s) you want. The sections will be recorded.

The following is a list of the sections, and the topic/problems covered.

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 | PDF Solutions |