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  Friday 

Jan 1216  Lecture 1: Introduction,
functional programming (numbers, lists), basic proofs Course information handout  Introductory slides Lecture notes  Basics.v (HW1) 
First recitation  
Jan 1923  Martin Luther King, Jr. Day (no class)  Lecture 2: Lists Lecture notes  Lists.v (HW2) HW1 due 

Jan 2630  Lecture 3: Polymorphism and higherorder functions, part 1 Poly_partial.v HW2 due 
Lecture 4: Polymorphism and higherorder functions, part 2 Lecture notes  Poly.v (HW3) 

Feb 26  Lecture 5: Induction; Logic, part 1 Partial lecture notes  Logic_partial.v HW3 due 
Lecture 6: Logic, part 2 Lecture notes  Ind.v 

Feb 913  Lecture 7: Logical Connectives Partial lecture notes  Logic_partial2.v HW4 due 
Lecture 8: Relations Lecture notes  Logic.v (HW5) 

Feb 1620  Review HW5 due 
Midterm I exam  solutions 

Feb 2327  Lecture 9: While programs, part 1 While_partial.v 
Lecture 10: While programs, part 2 While.v (HW6) 

Mar 26  Lecture 11: While programs  Program transformations Equiv_partial.v HW6 due 
Lecture 12: While programs  Transformation soundness and program verification Equiv.v (HW7) 

Mar 913  Spring break (no class)  
Mar 1620  Lecture 13: Hoare Logic, part 1 
Lecture 14: Hoare Logic, part 2 Hoare.v (HW8) HW7 due 

Mar 2327  Lecture 15: Smallstep operational semantics, part 1 
Lecture 16: SOS, part 2 Smallstep.v (HW09) HW8 due 

Mar 30Apr 3  Review Review notes HW9 due 
Midterm II exam  solutions 

Apr 610  Lecture 18: Types, part 1  Lecture 19: Types, part 2 Types.v (HW10) (HTML version) 

Apr 1317  Lecture 20: Types, part 3  Lecture 21: Types, part 4 MoreTypes.v (HW11) (HTML version); HW10 due 

Apr 2024  Lecture 22: Subtyping Subtyping.v (HTML version) 
No class  Last recitation 
Apr 27May 1  Lecture 23: Subtyping, part 2 Subtyping.v (HW12, due Sunday, May 3, at noon) (HTML); HW11 due 

May 48  Review session, 3:004:30, in Moore 212 
FINAL: Wednesday 6 May 911am Wu and Chen aud. solutions 