Mon, Wed 3:00-4:30PM
Towne 303
- Instructor
-
Benjamin C. Pierce
bcpierce AT cis.upenn.edu
office hours: Tuesdays 4-6pm in Levine 562 - Teaching Assistants
-
Chris Casinghino
ccasin AT cis.upenn.edu
office hours: Thursdays 3-4pm in Levine 565 -
Michael Greenberg
mgree AT cis.upenn.edu
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.
Schedule
| 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 Poly_partial.v 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 While_partial.v |
Lecture 10: While programs, part 2 While.v (HW6) |
|
| Mar 2-6 | Lecture 11: While programs - Program transformations Equiv_partial.v 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. solutions |
|