Certified Programming with Dependent Types

Harvard COMPSCI 252, Fall 2008

Instructors: Adam Chlipala, Greg Morrisett

Lectures: MW 3:00-4:30, Maxwell Dworkin 323 (time changed, based on scheduling discussion at first meeting!)

First Meeting: Monday, September 15

This class is about how to use the Coq proof assistant to get real work done, even on projects not focused on formal proofs or verification, by proving mechanically that your programs are correct. We will focus on dependent types and custom, scripted proof automation as means to this end. There will be a special focus on applications in programming languages and compilers, though most of the material will be relevant to mechanized theorem proving and certified programming in general.

[ More detailed course description ]

Prerequisites

Basic discrete math and logic; experience with functional programming, especially in statically-typed languages like Haskell and ML

Texts

• Online drafts of a book-in-progress specific to this course. The version of the book on this web site is frozen in its form from the end of this course. Consult the main book web site for newer versions.
• The Coq reference manual is also critical. We will try to focus the lectures and book chapters on material that is hard to glean from the manual, so using the manual to fill in the pieces is important.
• (Optional) The Coq'Art book might be useful, though we hope that students will have no trouble getting by without it.

Course Requirements

• Weekly problem sets, involving programming and proving in Coq (50% of grade)
• A course project, involving using Coq in some (hopefully publishable) research (30% of grade)
• Class participation (20% of grade)

Schedule