I. summary and review A. what to read in the rest of the book B. technical ideas what technical ideas did we discuss? Lambda calculus, capture, free variables, etc. operational semantics: big step vs. little step semantics type systems: rules, unique types subtyping, subsumption, variance properties, minimum types, subject reduction, type soundness, second-order (universal, existential types) equational logics C. intuitions Q: what intuitions did we discuss? Objects, fields, methods, dynamic dispatch, inheritance: delegation, embedding, traits, classes the Curry-Howard isomorphism (formula as types) types as sets, subtyping as subset inclusion D. relationships/questions Q: what kind of questions did we ask? Church-Rosser property of an operational semantics The soundness of type systems (subject reduction). equivalence of semantics, or translations unique typing, minimum typing The soundness and completeness of equational logics. E. limits Q: what are the limits of the theory that we've studied so far? Mostly uses the embedding model, doesn't deal with multimethods, concurrency, components, etc.