Optimal reductions in lambda calculus: Levy's formalization of the problem, Lamping's algorithm and its correctness. Connections to linear logic and geometry of interaction. Inherent complexity of implementing optimal reductions.
Categorical semantics of lambda calculus: Introduction to category theory. Cartesian closed categories and typed lambda calculus. Relation to deductive systems. Categories with reflexive elements, a construction by D. Scott.
Games semantics: Games semantics for lambda calculus. Solution to full abstraction problem via games. PCF, an extension of typed lambda calculus.