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 1014  Lecture: Introduction,
functional programming (numbers, lists), basic proofs Introductory slides Lecture notes: Preface, Basics  Basics.v (HW1) 

Jan 1721  Martin Luther King, Jr. Day (no class)  Lecture: Lists Lecture notes: Lists  Lists.v (HW2) HW1 due 
Jan 2428  Lecture: Polymorphism, functions as data Lecture notes: Poly  Poly.v 
Lecture: More About Coq Lecture notes: Poly  Poly.v (HW3) HW2 due 
Jan 31  Feb 4  Lecture: Propositions and evidence Lecture notes: Ind  Ind.v 
Lecture: Propositions and evidence (continued) Lecture notes: Ind  Ind.v (HW4) HW3 due 
Feb 711  Lecture: Logic in Coq Lecture notes: Logic  Logic.v 
Lecture: Logic in Coq Logic.v (HW5) HW4 due 
Feb 1418  Lecture: Review 
Midterm I
(exam,
solutions)
HW5 due 
Feb 2125  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 
Feb 27  March 4  Lecture: Program Equivalence Lecture notes: Equiv  Equiv.v 
Lecture: Program Equivalence, continued Lecture notes: Equiv  Equiv.v (HW7) HW6 due 
March 1418  Lecture: Hoare Logic Lecture notes: ImpList  ImpList.v  Hoare  Hoare.v 
Lecture: Hoare Logic, continued Lecture notes: ImpList  ImpList.v  Hoare  Hoare.v (HW8)  HW7 due 
March 2125  Lecture: SmallStep Semantics Lecture notes: Rel  Rel.v  Smallstep  Smallstep.v 
Lecture: SmallStep Semantics, continued Lecture notes: Rel  Rel.v  Smallstep  Smallstep.v (HW9) HW8 due 
March 28  April 1  Review  Midterm II
(exam,
solutions)
HW9 due 
April 48  Lecture: Simply Typed LambdaCalculus Lecture notes: Stlc  Stlc.v  
Lecture: STLC, continued Lecture notes: Stlc  Stlc.v (HW10, not including the "Properties" or "STLC with Arithmetic" sections) 
April 1113  Lecture: STLC, Continued Lecture notes: Stlc  Stlc.v  
Lecture: Extensions of STLC Lecture notes: MoreStlc  MoreStlc.v (HW11)  
April 1820  Lecture: References Lecture notes: References  References.v 
Lecture: References; Subtyping Lecture notes: References  References.v (HW12, part 1) Subtyping  Subtyping.v (HW12, part 2) 
April 25  Lecture: Subtyping, continued Lecture notes: Subtyping  Subtyping.v 

May 9  Final exam (911AM), Moore 216 (exam, solutions) 