Interactive Theorem Proving with Coq

Adam Chlipala
November 2, 2004
CS294-3: Techniques for Automated Deduction

  • Slides
  • Checking propostional logic proofs with the SML type checker: signature, implementation
  • Tutorial on basic proving
  • Proving the correctness of Java insertion sort: Java source, Coq source
  • Building an expression evaluator by compiling proofs to programs

    • Links

  • Coq
  • Why
  • Krakatoa