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