[PRL] Fwd: Coq class this fall at Harvard

[Mitchell Wand]

---------- Forwarded message ----------
From: Adam Chlipala <adamc at hcoop.net>
Date: Fri, Sep 5, 2008 at 4:07 PM
Subject: Coq class this fall at Harvard
To: arvind at csail.mit.edu, matthias at ccs.neu.edu, pete at ccs.neu.edu,
riccardo at ccs.neu.edu, nr at cs.tufts.edu, rinard at lcs.mit.edu,
shivers at ccs.neu.edu, fturbak at wellesley.edu, Mitchell Wand <wand at ccs.neu.edu>,
hwxi at cs.bu.edu
Cc: Greg Morrisett <greg at eecs.harvard.edu>


I'm teaching a class at Harvard this fall on effective engineering with the
Coq proof assistant, with a focus on proofs about programming languages and
compilers.  Greg Morrisett suggested e-mailing you, in case you or your
students might be interested in participating.  Everyone is welcome.

The essential data on the course are below.  At the first meeting, we will
discuss whether another time would work better for the people who are
interested in coming.

Web site: http://www.cs.harvard.edu/~adamc/cpdt/<http://www.cs.harvard.edu/%7Eadamc/cpdt/>
Harvard course number: COMPSCI 252
Lectures: MW 2-4, Maxwell Dworkin 323
First Meeting: Monday, September 15

Course Description:

This class is about building programs with machine-checked proofs of
functional correctness.  Techniques like model checking enable
mostly-automated verification of shallow properties of deep programs.  Our
focus in this class will be on verifying deep properties of small- to
medium-sized programs, using interactive proof assistants.  In particular,
we will focus on the Coq proof assistant, which, together with its
associated tools, serves as a (perhaps surprisingly, to most people) quite
mature development environment for programming with specifications.  The
goal of this class is to convince you that you (yes, you!) can start using
Coq today to build verified programs, with an increase in effort over
traditional programming that is justified by the formal correctness theorems
you end up with.

The focus of the class will be on engineering best practices for certified
programming and interactive theorem proving.  Just what these practices are
is far from a settled question, but we'll do our best to maximize
programmer/prover productivity and promote readability and maintainability
of the results.  We plan to push one particular recipe for this that almost
no one is using yet: dependent types plus custom-tailored proof automation.

Dependent type systems allow types that refer to programs.  The
possibilities of this idea are pretty mind-boggling, ranging from assigning
array deference a type guaranteeing no out-of-bounds references, to
assigning a compiler a type that guarantees that its output programs have
the same observable behavior as its input programs.  Putting dependent types
to use requires a lot of theory, a lot of tool construction, and a good
amount of experience with basic "design patterns."  Luckily for us, Coq
already provides the first two.  One of the big aims of this class is to
provide the third.

With dependent types, you can often "prove" important properties of your
programs with almost no additional effort beyond writing the program
normally, when you manage to find appropriate dependent types to assign.
 When this works, what you've discovered is that there is a correctness
proof that mirrors the structure of your program.  For many interesting
verification problems, no such proofs exist.  For instance, a compiler
correctness proof must follow the structure of program executions, which may
follow neither the structure of the compiler nor the structure of the
programs it processes.

Coq provides a very general "proof script" facility for writing out manual
proofs of such theorems.  It's a safe approximation to say that any
mathematical proof can be formalized in this way.  Most of the current and
historical work with proof assistants for higher-order languages has used
very manual proof approaches.  With proof assistants like Coq and
Isabelle/HOL, we have "proof by video game," where the human prover
alternates between reading dumps of proof state and entering short commands
to simplify the goal.  The final results tend to be impossible to understand
without replaying the proof step by step.  With proof assistants like Twelf,
the situation is worse for initial proving, as the proofs people write in
practice are essentially isomorphic to formal natural deduction proofs in
full gory detail.  The results are more structured and thus more readable in
that sense, but the extreme level of detail can be just as
confusion-inducing as extreme lack of structure.

In this class, we'll focus instead on a style that we call "proof by
decision procedure."  Coq includes a Turing-complete language for writing
programs that manipulate proof states, such that, by construction, one of
these programs can never claim to have proved a goal when it really hasn't.
 We will show how many examples of certified programming can be completed by
writing custom decision procedures that are robust to changes in program
implementation and specification.  Proofs in this style are naturally
decomposed into pieces that can be read and understood in isolation, free of
deep hierarchical structure, a major victory for maintainability.

We expect to spend almost all of class time on example programs and proofs,
with the class working together to build the solutions in a live Coq
environment.  We'll draw examples from a variety of domains, based on
audience interest.  We'll probably spend a good amount of time on
applications related to certified programming language tools, since they
provide a great stress test for reasoning about programs with complicated
specifications, and also because the instructor thinks they're cool.


==================================
Incomplete list of topics to cover
==================================

* A simple compiler from a binder-free language to a stack machine, and its
mostly-automated proof
* Crash course on basic tactics for manual proofs
* Crash course on induction and its pitfalls in Coq
* Infinite data objects and proofs via co-inductive types
* Programming with subset types and refinement
* Introduction to more dependent types
* Alternatives for defining dependent datatypes
* Introduction to Ltac, Coq's Turing-complete tactic language
* Pattern matching and backtracking in Coq tactics
* Proof by reflection (AKA putting certified decision procedures to work)
* Proving things about programs that use type equality proofs
* Techniques for representing variable binders
 * First-order techniques: concrete names, De Bruijn indices, locally
nameless
 * Higher-order abstract syntax, and how to get most of its benefits in Coq
* Language semantics by definitional compilers
* Building certified program transformations
 * Extensional transformations, e.g., CPS conversion
 * Intensional transformations, e.g., closure conversion
* Semantics and certified transformations for languages with general
recursion and side effects
* Ynot: Imperative programming with specifications in Coq
-------------- next part --------------
HTML attachment scrubbed and removed