This course will examine the design and implementation of programming
languages from a foundational perspective. Our goal will be to
develop tools that will enable us to both design and specify new
language features, to precisely understand the rationale for existing
features in modern languages, and to understand how design decisions
can impact implementations. The course will be divided into roughly
three parts: (1) principles (e.g., semantics, type systems, specifications);
(2) proof techniques and formal reasoning and (3) automated theorem proving
using the Coq proof assistant. Our discussion of principles will be
crafted in the context of definitions and theorems that capture salient
properties of modern languages. The validation of these theorems will be
undertaken using Coq, a powerful theorem prover and mechanized proof
assistant.
All assignments and course lectures will take place using the mechanized proof assistant, Coq.
You will need to download version 8.4, as well as an editor to facilitate
writing interactive proofs. Proof General (which works
with Emacs) and CoqIde, a standalone graphical editor are both
good choices.
The course text is Software Foundations.
We will follow the material in the text closely. Each lecture will cover the
material in the chapter by reviewing the corresponding source code and proofs.