Simply-typed lambda calculus Untyped lambda calculus Evaluation strategies Typing relation Contexts Generation lemma Uniqueness of types Progress Subject reduction Church-style vs. Curry-style