Introduction to the theory of programming languages. How to define programming languages using operational semantics and type systems, and how to prove things about them. Starting with the lambda calculus as a core, a simple programming language is built up, with higher-order functions and lexical scope; algebraic data types, polymorphic types, and type inference; state and control. Students will also gain experience with functional programming and writing interpreters.

This course is planned to be offered in Spring 2019. It will join a “trilogy” of courses on programming languages, the other two being *Programming Paradigms* (CSE 30332) and *Compilers and Language Design* (CSE 40243). Whereas *Paradigms* is about using programming languages and *Compilers* is about implementing programming languages, this course is about programming language **semantics**, which bridges the other two by defining, in a mathematical way, what programming languages mean.