In no particular order: - big-step and small-step semantics - evaluation context - type context - STLC - System F - (somewhat advanced) difference between Gamma (types of program variables, that is lambda abstractions) vs Delta (type variables)