Mon, Wed 3:00-4:30PM
Towne 303
- Instructor
-
Benjamin C. Pierce
bcpierce AT cis.upenn.edu
office hours: by appointment - Teaching Assistants
-
Vilhelm Sjöberg
vilhelm AT cis.upenn.edu
office hours: Tuesdays, 4-6 in Moore 207 -
Brent Yorgey
byorgey AT cis.upenn.edu
office hours: Mondays, 5-7 in Moore 100A
Text
The main text for the course is the online book Software Foundations. Recommendations for some useful supplemental texts 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 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 |
|---|---|---|
| Jan 11-15 | Lecture: Introduction,
functional programming (numbers, lists), basic proofs Introductory slides Lecture notes: Preface, Basics | Basics.v (HW1) |
|
| Jan 18-22 | Martin Luther King, Jr. Day (no class) | Lecture: Lists Lecture notes: Lists | Lists.v (HW2) HW1 due |
| Jan 25-29 | Lecture: Polymorphism, functions as data Lecture notes: Poly | Poly.v |
Lecture: More About Coq Lecture notes: Poly | Poly.v (HW3) HW2 due |
| Feb 1-5 | Lecture: Propositions and evidence Lecture notes: Ind | Ind.v |
Lecture: Propositions and evidence (continued) Lecture notes: Ind | Ind.v (HW4) HW3 due |
| Feb 8-12 | Lecture: Logic in Coq Lecture notes: Logic | Logic.v |
Lecture: cancelled due to weather Logic.v (HW5) HW4 due |
| Feb 15-19 | Lecture: Review Lecture notes: Template for informal proofs |
Midterm I (exam,
solutions) HW5 due |
| Feb 22-26 | 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) | ImpParser | ImpParser.v | SfLib.v |
| March 1-5 | Lecture: Program Equivalence Lecture notes: Equiv | Equiv.v |
Lecture: Program Equivalence, continued Lecture notes: Equiv | Equiv.v (HW7) |
| March 15-19 | Lecture: Hoare Logic Lecture notes: Hoare | Hoare.v |
Lecture: Hoare Logic, continued Lecture notes: Hoare | Hoare.v (HW8) | MoreHoare | MoreHoare.v (HW8) |
| March 22-26 | Lecture: Small-Step Semantics Lecture notes: Rel | Rel.v | Smallstep | Smallstep.v You'll also need updated versions of SfLib.v and Imp.v |
Lecture: Small-Step Semantics, continued Lecture notes: Smallstep | Smallstep.v (HW9) For the HW, you'll also need updated versions of SfLib.v and Imp.v |
| March 29 - April 2 | Review | Midterm II (exam, solutions) |
| April 5-9 | Lecture: Simply Typed Lambda-Calculus Lecture notes: Stlc | Stlc.v | |
Lecture: STLC, continued Lecture notes: Stlc | Stlc.v (HW10) |
| April 12-14 | Lecture: STLC, Continued Lecture notes: MoreStlc | MoreStlc.v | |
Lecture: STLC, References Lecture notes: MoreStlc | MoreStlc.v (HW11) | References | References.v |
| April 19-21 | Lecture: References, continued Lecture notes: References | References.v |
Lecture: References; Subtyping Lecture notes: References | References.v (HW12, part 1) Subtyping | Subtyping.v (HW12, part 2) |
| April 26 | Lecture: Subtyping, continued Lecture notes: Subtyping | Subtyping.v |
|
| May 3 | Final: exam, answers |