CIS 500: Software Foundations - Spring 2009

Picture of TAPL

Mon, Wed 3:00-4:30PM

Towne 303

Benjamin C. Pierce
bcpierce_NOSPAM AT
office hours: Tuesdays 4-6pm in Levine 562
Teaching Assistants
Chris Casinghino
ccasin_NOSPAM AT
office hours: Thursdays 3-4pm in Levine 565
Michael Greenberg
office hours: Mondays 11-12am in Levine 571

Homework submission

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 12-16 Lecture 1: Introduction, functional programming (numbers, lists), basic proofs
Course information handout | Introductory slides
Lecture notes | Basics.v (HW1)
First recitation
Jan 19-23 Martin Luther King, Jr. Day (no class) Lecture 2: Lists
Lecture notes | Lists.v (HW2) HW1 due
Jan 26-30 Lecture 3: Polymorphism and higher-order functions, part 1
HW2 due
Lecture 4: Polymorphism and higher-order functions, part 2
Lecture notes | Poly.v (HW3)
Feb 2-6 Lecture 5: Induction; Logic, part 1
Partial lecture notes | Logic_partial.v
HW3 due
Lecture 6: Logic, part 2
Lecture notes | Ind.v
Feb 9-13 Lecture 7: Logical Connectives
Partial lecture notes | Logic_partial2.v
HW4 due
Lecture 8: Relations
Lecture notes | Logic.v (HW5)
Feb 16-20 Review
HW5 due
Midterm I
exam | solutions
Feb 23-27 Lecture 9: While programs, part 1
Lecture 10: While programs, part 2
While.v (HW6)
Mar 2-6 Lecture 11: While programs - Program transformations
HW6 due
Lecture 12: While programs - Transformation soundness and program verification
Equiv.v (HW7)
Mar 9-13 Spring break (no class)
Mar 16-20 Lecture 13: Hoare Logic, part 1
Lecture 14: Hoare Logic, part 2
Hoare.v (HW8)
HW7 due
Mar 23-27 Lecture 15: Small-step operational semantics, part 1

Lecture 16: SOS, part 2
Smallstep.v (HW09)
HW8 due
Mar 30-Apr 3 Review
Review notes
HW9 due
Midterm II
exam | solutions
Apr 6-10 Lecture 18: Types, part 1 Lecture 19: Types, part 2
Types.v (HW10) (HTML version)
Apr 13-17 Lecture 20: Types, part 3 Lecture 21: Types, part 4
MoreTypes.v (HW11) (HTML version); HW10 due
Apr 20-24 Lecture 22: Subtyping
Subtyping.v (HTML version)
No class Last recitation
Apr 27-May 1 Lecture 23: Subtyping, part 2
Subtyping.v (HW12, due Sunday, May 3, at noon) (HTML);
HW11 due
May 4-8 Review session, 3:00-4:30, in Moore 212 FINAL: Wednesday 6 May 9-11am
Wu and Chen aud.