Mercurial > cpdt > repo

comparison syllabus.txt @ 1:0ba25681a11b

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