Class 1: Overview * Arithmetic expressions * Arithmetic expressions with let-binding o Variation: Call-by-value let-binding syntax o Variation: Defining evaluation with a hypothetical judgement * Typed arithmetic expressions o Variation: Typed arithmetic expressions (extrinsic encoding) * Exercises 1 Class 2: Representation * Mechanizing Metatheory in a Logical Framework discusses this material in detail. * Exercises 2 Class 3: Mechanizing Metatheory * Type safety for MinML (intrinsic encoding) * Type safety for MinML (extrinsic encoding) * Exercises 3 Additional reading * PFPL: We will use Practical Foundations for Programming Languages as a reference for basic PL concepts. * MMLF: Mechanizing Metatheory in a Logical Framework discusses LF, representation, and mechanized metatheory in technical detail. * Proving metatheorems with Twelf is a self-contained intro tutorial