Fundamentals of programming language design and theory. Topics include formal semantics and type systems for imperative, functional, and parallel languages; lambda calculus and its variants; the Curry-Howard Correspondence; techniques for proving language properties and verifying program specifications.