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

Jan 1620  Martin Luther King, Jr. Day (no class)  Lecture: Lists Lecture notes: Lists  Lists.v (HW2) HW1 due 
Jan 2327  Lecture: Polymorphism, functions as data Lecture notes: Poly  Poly.v 
Lecture: More About Coq Lecture notes: Poly  Poly.v (HW3) HW2 due 
Jan 30  Feb 3  Lecture: Propositions and evidence Lecture notes: Gen  Gen.v  Prop  Prop.v 
Lecture: Propositions and evidence (continued) Lecture notes: Gen  Gen.v  Prop  Prop.v (HW4) HW3 due 
Feb 610  Lecture: Logic in Coq Lecture notes: Logic  Logic.v 
Lecture: Logic in Coq Logic.v (HW5) HW4 due 
Feb 1317  Lecture: Review 
Midterm I
(exam,
solutions)
HW5 due 
Feb 2024  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 27  March 2  Lecture: Program Equivalence Lecture notes: Equiv  Equiv.v 
Lecture: Program Equivalence, continued Lecture notes: Equiv  Equiv.v (HW7) HW6 due 
March 59  Spring Break (no class)  Spring Break (no class) 
March 1216  Lecture: Hoare Logic Lecture notes: ImpList  ImpList.v  Hoare  Hoare.v 
Lecture: Hoare Logic, continued Lecture notes: ImpList  ImpList.v  Hoare  Hoare.v (HW8)  HoareDec  HoareDec.v HW7 due 
March 1923  Lecture: Hoare Logic, continued Lecture notes: HoareDec  HoareDec.v 
Lecture: Hoare Logic, continued Lecture notes: HoareDec  HoareDec.v (HW9)  Rel  Rel.v  HW8 due 
March 26  30  Review  Midterm II
(exam,
solutions)
HW9 due 
April 26  Lecture: SmallStep Semantics Lecture notes: Rel  Rel.v  Smallstep  Smallstep.v 
Lecture: SmallStep Semantics, continued Lecture notes: Rel  Rel.v  Smallstep  Smallstep.v (HW10) 
April 911  Lecture: Types Lecture notes: Types  Types.v (HW11, part 1)  
Lecture: Simply Typed LambdaCalculus Lecture notes: Stlc  Stlc.v (HW11, part 2  omitting the "Properties" and "STLC with Arithmetic" sections) 
April 1620  Lecture: STLC, continued Lecture notes: Stlc  Stlc.v (HW12, part 1)  MoreStlc  MoreStlc.v (HW12, part 2)  
Lecture: Subtyping Lecture notes: Sub  Sub.v 
April 23  Lecture: Subtyping, continued Lecture notes: Sub  Sub.v 

May 3 (Thursday)  Final exam (911AM) (exam, solutions) 