Mon, Wed 3:00-4:30PM
Towne 303
- Instructor
-
Benjamin C. Pierce
bcpierce AT cis.upenn.edu
office hours: TBA - Teaching Assistants
-
Anthony Cowley
acowley AT seas.upenn.edu
office hours: Mondays, 5-7pm, Moore 100A -
Brent Yorgey
byorgey AT cis.upenn.edu
office hours: Tuesdays, 6-8pm, Moore 100A
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 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.
Tentative Schedule
| Week | Monday | Wednesday |
|---|---|---|
| Jan 10-14 | Lecture: Introduction,
functional programming (numbers, lists), basic proofs Introductory slides Lecture notes: Preface, Basics | Basics.v (HW1) |
|
| Jan 17-21 | Martin Luther King, Jr. Day (no class) | Lecture: Lists Lecture notes: Lists | Lists.v (HW2) HW1 due |
| Jan 24-28 | Lecture: Polymorphism, functions as data Lecture notes: Poly | Poly.v |
Lecture: More About Coq Lecture notes: Poly | Poly.v (HW3) HW2 due |
| Jan 31 - Feb 4 | Lecture: Propositions and evidence Lecture notes: Ind | Ind.v |
Lecture: Propositions and evidence (continued) Lecture notes: Ind | Ind.v (HW4) HW3 due |
| Feb 7-11 | Lecture: Logic in Coq Lecture notes: Logic | Logic.v |
Lecture: Logic in Coq Logic.v (HW5) HW4 due |
| Feb 14-18 | Lecture: Review |
Midterm I
(exam,
solutions)
HW5 due |
| Feb 21-25 | 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 |
| Feb 27 - March 4 | Lecture: Program Equivalence Lecture notes: Equiv | Equiv.v |
Lecture: Program Equivalence, continued Lecture notes: Equiv | Equiv.v (HW7) HW6 due |
| March 14-18 | Lecture: Hoare Logic Lecture notes: ImpList | ImpList.v | Hoare | Hoare.v |
Lecture: Hoare Logic, continued Lecture notes: ImpList | ImpList.v | Hoare | Hoare.v (HW8) | HW7 due |
| March 21-25 | 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 (HW9) HW8 due |
| March 28 - April 1 | Review | Midterm II
(exam,
solutions)
HW9 due |
| April 4-8 | Lecture: Simply Typed Lambda-Calculus Lecture notes: Stlc | Stlc.v | |
Lecture: STLC, continued Lecture notes: Stlc | Stlc.v (HW10, not including the "Properties" or "STLC with Arithmetic" sections) |
| April 11-13 | Lecture: STLC, Continued Lecture notes: Stlc | Stlc.v | |
Lecture: Extensions of STLC Lecture notes: MoreStlc | MoreStlc.v (HW11) | |
| April 18-20 | Lecture: References Lecture notes: References | References.v |
Lecture: References; Subtyping Lecture notes: References | References.v (HW12, part 1) Subtyping | Subtyping.v (HW12, part 2) |
| April 25 | Lecture: Subtyping, continued Lecture notes: Subtyping | Subtyping.v |
|
| May 9 | Final exam (9-11AM), Moore 216 (exam, solutions) |