This course will examine the design and implementation of programming
languages from a semantics-based perspective. Our goal will be to
develop tools that will enable us to both design and specify new
language features, formally understand the implications of such designs,
explain the rationale for existing
features in modern languages, and develop mechanisms that allow us to
prove interesting properties of langauge implementations.
. The course consists of three broad components: (1) principles
(e.g., semantics, type systems, specifications);
(2) proof techniques and formal reasoning and (3) mechanized 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 leverage
proof techniques such as induction expressed using Coq, a powerful theorem prover and mechanized proof
assistant.
All assignments and course lectures will use Coq.
You will need to download version
8.5, 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 being discussed by reviewing the corresponding source code and proofs.