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!


  • 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


    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