This core course is about techniques for analyzing and understanding software artifacts. Ultimately, the goal of this area of study is to improve the quality of software. We will cover three related areas of programming languages research:

1.Static analysis, the name for any automatic technique for reasoning about program source code. We will study data flow analysis, type systems, and other forms of analysis.

2.Formal systems for describing languages and programs, including lambda calculus and axiomatic, denotational, and operational semantics. We will be encoding these semantics in part with the Coq proof assistant.

3.Programming language features and how they affect software, including imperative, functional, and object-oriented programming.