Section Notes CS430/530: Formal Semantics, Fall 2009, Yale University

Section 1 (Sep 11): Theorem proving with Coq

• Section slides and notes.
• The tutorial Coq development we showed with comments, without comments and without proofs.
• The Coq home page.
• To use Coq in the zoo machines, add the following line to your .bash_profile :
  export PATH=$PATH:/c/cs430/bin
  Now you can use either coqide or proofgeneral. To compile a Coq development (e.g. if it is required by another development) you can use coqc.
• Additional Coq resources: the official Coq tutorial, the reference manual, the documentation of the standard library, Coq'Art, and Certified Programming with Dependent Types.
• A sample development of the proofs of chapter A.2 of Reynolds' appendix: definitions, proofs using the declarative proof style, proofs relying on automatic tactics.