Mon, Wed 3:00-4:30PM
Moore 216
- Instructor
-
Benjamin C. Pierce
bcpierce AT cis.upenn.edu
Office hours: Mondays, 4:30 - 6:00, Levine 562 - Teaching Assistants
-
Catalin Hritcu
catalin.hritcu AT gmail.com
Office hours: Tuesdays, 4 - 6, Moore 207 lab -
Mukund Raghothaman
rmukund AT seas.upenn.edu
Office hours: Tuesdays, 6 - 8, Moore 207 lab -
Loris D'Antoni
lorisdan AT seas.upenn.edu
Office hours: Fridays, 3 - 5, location TBA
Text
The main text for the course is the online book Software Foundations. A good supplemental text is Types and Programming Languages (Pierce). Recommendations for some other useful books can be found in the preface.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 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.
Tentative Schedule
| Week | Monday | Wednesday |
|---|---|---|
| Jan 9-13 | Lecture: Introduction,
functional programming (numbers, lists), basic proofs Introductory slides Lecture notes: Preface, Basics Homework: Basics.v (HW1) |
|
| Jan 16-20 | Martin Luther King, Jr. Day (no class) | Lecture: Lists Lecture notes: Lists | Lists.v (HW2) HW1 due |
| Jan 23-27 | 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 6-10 | Lecture: Logic in Coq Lecture notes: Logic | Logic.v |
Lecture: Logic in Coq Logic.v (HW5) HW4 due |
| Feb 13-17 | Lecture: Review |
Midterm I
(exam,
solutions)
HW5 due |
| Feb 20-24 | 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 5-9 | Spring Break (no class) | Spring Break (no class) |
| March 12-16 | 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 19-23 | 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 2-6 | Lecture: Small-Step Semantics Lecture notes: Rel | Rel.v | Smallstep | Smallstep.v |
Lecture: Small-Step Semantics, continued Lecture notes: Rel | Rel.v | Smallstep | Smallstep.v (HW10) |
| April 9-11 | Lecture: Types Lecture notes: Types | Types.v (HW11, part 1) | |
Lecture: Simply Typed Lambda-Calculus Lecture notes: Stlc | Stlc.v (HW11, part 2 -- omitting the "Properties" and "STLC with Arithmetic" sections) |
| April 16-20 | 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 (9-11AM) (exam, solutions) |