Interactive Computer Theorem Proving Administrivia
(CS294-9 Fall 2006)
Instructors: Adam Chlipala and George Necula.
When: Thursday 2:00-3:30 in Soda 310.
This class is a complement to the class on automated first-order theorem proving. We'll keep the "theorem proving" part and tweak "automated" and "first-order". Higher-order logics based on type theory, with strong connections to functional programming are powerful enough to allow the effective expression of most of mathematics, and they can also be used as the bases of environments for programming with specifications and correctness proofs. Unsurprisingly, this makes the truth of formulas undecidable, which is where the "interactive" part comes in. We will look at proof assistants like Coq that provide rich languages for describing the structures of proofs at varying levels of detail, where the proof assistant is responsible for filling in everything you leave out.
This class is aimed at an audience more interested in practice than theory, and so we hope to avoid the standard examples from pure math when possible. If you have in mind some potential examples relevant to your work, please let me know!
Organization
Weekly 80-minute lectures
Four to eight homework assignments, associated with roughly the first half of the course, involving using Coq to formalize concepts and prove theorems about them
For the second half, a standard project component where you use interactive theorem proving as part of the research project of your choice
The course can be taken for either 1 or 3 units, the latter applicable if you do the semester project.
Topics
- Roadmap of the world of formal logic tools
- Coq
- Basic interactive proof of propositional and first-order theorems
- Basic inductive types for functional data structures
- Proof terms and the Curry-Howard Isomorphism
- Advanced uses of tactics for proof automation
- Proof by reflection, or why having a programming language as part of your logic is a good thing
- Programming with specifications
- Program extraction to ML
- Case studies
- Formalizing a complete programming language and a certified interpreter?
- Twelf
- The LF meta-logic and why you'd want to use it (canonical forms, etc.)
- Thinking about proofs as logic programs
- Higher-order abstract syntax
- Recent projects
- Integrating programming-with-proofs with nastier programming language features like mutable state and non-termination (e.g., ATS, RSP, Omega)
- More?
Books
I'm going to try to avoid any need to use references that aren't available online, but this book could be helpful and is worth reading if you want to pursue using this stuff:
Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions)
Software
Here are a few interactive theorem proving tools for higher-order logics that are available online.
Coq
Isabelle
Twelf