annotate syllabus.txt @ 1:0ba25681a11b

Possible class topics
author Adam Chlipala <adamc@hcoop.net>
date Wed, 20 Aug 2008 11:23:02 -0400
parents 433ef87f6057
children
rev   line source
adamc@0 1 ==========================================
adamc@0 2 Certified Programming with Dependent Types
adamc@0 3 ==========================================
adamc@0 4
adamc@0 5 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.
adamc@0 6
adamc@0 7 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.
adamc@0 8
adamc@0 9 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.
adamc@0 10
adamc@0 11 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.
adamc@0 12
adamc@0 13 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.
adamc@0 14
adamc@0 15 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.
adamc@0 16
adamc@1 17 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. We also hope to spend a lot of the class on case studies suggested by participants based on their own research and other interests.
adamc@0 18
adamc@1 19
adamc@1 20 ================================================
adamc@1 21 Topics to cover in whole class periods or longer
adamc@1 22 ================================================
adamc@1 23
adamc@1 24 * A simple compiler from a binder-free language to a stack machine, and its mostly-automated proof
adamc@1 25 * Crash course on basic tactics for manual proofs
adamc@1 26 * Crash course on induction and its pitfalls in Coq
adamc@1 27 * Infinite data objects and proofs via co-inductive types
adamc@1 28 * Programming with subset types and refinement
adamc@1 29 * Introduction to more dependent types
adamc@1 30 * Alternatives for defining dependent datatypes
adamc@1 31 * Introduction to Ltac, Coq's Turing-complete tactic language
adamc@1 32 * Pattern matching and backtracking in Coq tactics
adamc@1 33 * Proof by reflection (AKA putting certified decision procedures to work)
adamc@1 34 * Proving things about programs that use type equality proofs
adamc@1 35 * Techniques for representing variable binders
adamc@1 36 * First-order techniques: concrete names, De Bruijn indices, locally nameless
adamc@1 37 * Higher-order abstract syntax, and how to get most of its benefits in Coq
adamc@1 38 * Language semantics by definitional compilers
adamc@1 39 * Building certified program transformations
adamc@1 40 * Extensional transformations, e.g., CPS conversion
adamc@1 41 * Intensional transformations, e.g., closure conversion
adamc@1 42 * Semantics and certified transformations for languages with general recursion and side effects
adamc@1 43 * Ynot: Imperative programming with specifications in Coq
adamc@1 44
adamc@1 45 * Student project presentations