Mathematical tools for relating syntactic structure to semantic interpretation. Topics include higher-order logic, lambda calculus, intensional logic, type theory, type-driven translation, type lifting, and lattices.

Prerequisite: 16:615:530