Sections are held:

• Friday 12:15–1:15pm in SEC LL2.221 (subject to change), led by Paula and Jonas
• Tuesday 4:00–5:00pm in room TBA, led by Emma and including Coq.

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