Modern proof assistants, such as
Coq,
Twelf and
Isabelle,
are mature tools that have been used to create significant bodies of
formalized mathematics. Instead of proving theorems
automatically, these tools have achieved great success by working
interactively, verifying the small steps of formal reasoning but
leaving the main argument of the proof to be supplied. These tools are
exactly what the designers of modern programming languages need. They
provide a way to formally express the semantics of a modern programming
language (at a higher-level than a compiler or interpreter, but more
concretely than with English prose) and verify important properties
(such as type soundness) about that design.
The goal of this course
is to study the
foundations for and current practice
with modern proof assistants in the context of programming
language research. We will learn to use these tools well by studying
the type theory that they are based on. The format will be as a
discussion course, with grades coming from presentations, class
participation and a semester project. Anyone who has taken CIS 500
should be able to take this course.