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, 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 at noon on the date specified. 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 711  Lecture: Introduction,
functional programming Opening slides Lecture notes: Preface, Basics Homework: Basics.v (HW1) 

Jan 1418  Lecture: Induction, Lists Opening slides Lecture notes: Induction, Lists 
Lecture: Lists, Polymorphism Lecture notes: Lists, Poly Homework: Induction.v and Lists.v (HW2) 
Jan 2125  Martin Luther King, Jr. Day (no class)  Lecture: Polymorphism, functions as data, more about Coq Lecture notes: Poly  Poly.v (HW3) HW2 due at noon 
Jan 28  Feb 1  Lecture: More About Coq Lecture notes: MoreCoq  MoreCoq.v  
Lecture: Propositions and evidence Lecture notes: Prop Homework: MoreCoq.v and Prop.v (HW4) HW3 due at noon 
Feb 48  Lecture: Logic in Coq Lecture notes: MoreProp  MoreProp.v Logic  Logic.v  MoreInd  MoreInd.v 
Lecture: Logic in Coq (continued) MoreProp.v, Logic.v, and MoreInd.v (HW5) HW4 due at noon 
Feb 1115  Lecture: Review Review problems 
Midterm I
(Standard version,
Advanced version,
Answers)
HW5 due at noon 
Feb 1822  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)  SfLib.v (needed for HW6) Supplementary files: ImpParser  ImpParser.v  ImpCEvalFun  ImpCEvalFun.v 
Feb 25  March 1  Lecture: Program Equivalence Lecture notes: Equiv  Equiv.v 
Lecture: Program Equivalence, continued Lecture notes: Equiv  Equiv.v (HW7) HW6 due at noon 
March 48  Spring Break (no class)  Spring Break (no class) 
March 1115  Lecture: Hoare Logic Lecture notes: Hoare  Hoare.v 
Lecture: Hoare Logic, continued Lecture notes: Hoare  Hoare.v (HW8)  HW7 due at noon 
March 1822  Lecture: Hoare Logic, continued Lecture notes: Hoare2.v 
Lecture: Hoare Logic, continued Lecture notes: Hoare2  Hoare2.v (HW9)  HW8 due at noon 
March 25  29  Lecture: Review Review problems 
Midterm II
(Standard version,
Advanced version,
Answers)
HW9 due at noon 
April 15  Lecture: SmallStep Semantics Lecture notes: Smallstep  Smallstep.v 
Lecture: SmallStep Semantics, continued Lecture notes: Smallstep  Smallstep.v (HW10) 
April 812  Lecture: Types Lecture notes: Auto  Auto.v  Types  Types.v (HW11, part 1)  
Lecture: Simply Typed LambdaCalculus Lecture notes: Stlc  Stlc.v (HW11, part 2) 
April 1519  Lecture: STLC, continued Lecture notes: StlcProp  StlcProp.v (HW12, part 1)  MoreStlc  MoreStlc.v (HW12, part 2)  
Lecture: Subtyping Lecture notes: Sub  Sub.v 
April 22  Lecture: Subtyping, continued Lecture notes: Sub  Sub.v 

Tuesday, April 30  Final exam (911AM), DRLB A6 (Standard version, Standard with answers, Advanced version, Advanced with answers) 