Homework can be submitted via Blackboard. If you are taking the course but cannot access the CIS 500 Blackboard, please contact one of the TAs.
When submitting Coq files as homeworks, please make sure that Coq accepts your file in its entirety. If it does not, it will not be graded. You can use Admitted to force Coq to accept incomplete proofs.
Homework is due before class. Late homework submissions will be accepted for up to three days, with a 25% reduction in credit per late day (25% for one day, 50% for two, and 75% for three). Solutions will be posted on Blackboard.
Week  Monday  Wednesday 

Jan 1115  Lecture: Introduction,
functional programming (numbers, lists), basic proofs Introductory slides Lecture notes: Preface, Basics  Basics.v (HW1) 

Jan 1822  Martin Luther King, Jr. Day (no class)  Lecture: Lists Lecture notes: Lists  Lists.v (HW2) HW1 due 
Jan 2529  Lecture: Polymorphism, functions as data Lecture notes: Poly  Poly.v 
Lecture: More About Coq Lecture notes: Poly  Poly.v (HW3) HW2 due 
Feb 15  Lecture: Propositions and evidence Lecture notes: Ind  Ind.v 
Lecture: Propositions and evidence (continued) Lecture notes: Ind  Ind.v (HW4) HW3 due 
Feb 812  Lecture: Logic in Coq Lecture notes: Logic  Logic.v 
Lecture: cancelled due to weather Logic.v (HW5) HW4 due 
Feb 1519  Lecture: Review Lecture notes: Template for informal proofs 
Midterm I (exam,
solutions) HW5 due 
Feb 2226  Lecture: Coq automation and while programs Lecture notes: Imp  Imp.v  ImpParser  ImpParser.v  SfLib.v 
Lecture: While programs Lecture notes: Imp  Imp.v (HW6)  ImpParser  ImpParser.v  SfLib.v 
March 15  Lecture: Program Equivalence Lecture notes: Equiv  Equiv.v 
Lecture: Program Equivalence, continued Lecture notes: Equiv  Equiv.v (HW7) 
March 1519  Lecture: Hoare Logic Lecture notes: Hoare  Hoare.v 
Lecture: Hoare Logic, continued Lecture notes: Hoare  Hoare.v (HW8)  MoreHoare  MoreHoare.v (HW8) 
March 2226  Lecture: SmallStep Semantics Lecture notes: Rel  Rel.v  Smallstep  Smallstep.v You'll also need updated versions of SfLib.v and Imp.v 
Lecture: SmallStep Semantics, continued Lecture notes: Smallstep  Smallstep.v (HW9) For the HW, you'll also need updated versions of SfLib.v and Imp.v 
March 29  April 2  Review  Midterm II (exam, solutions) 
April 59  Lecture: Simply Typed LambdaCalculus Lecture notes: Stlc  Stlc.v  
Lecture: STLC, continued Lecture notes: Stlc  Stlc.v (HW10) 
April 1214  Lecture: STLC, Continued Lecture notes: MoreStlc  MoreStlc.v  
Lecture: STLC, References Lecture notes: MoreStlc  MoreStlc.v (HW11)  References  References.v 
April 1921  Lecture: References, continued Lecture notes: References  References.v 
Lecture: References; Subtyping Lecture notes: References  References.v (HW12, part 1) Subtyping  Subtyping.v (HW12, part 2) 
April 26  Lecture: Subtyping, continued Lecture notes: Subtyping  Subtyping.v 

May 3  Final: exam, answers 