Mon, Wed 3:00-4:30PM
Moore 216
- Instructor
-
Benjamin C. Pierce
bcpierce AT cis.upenn.edu
Office hours: Monday 4:30 to 6, Levine 562 - Teaching Assistants
-
Arthur Azevedo de Amorim
aarthur AT seas.upenn.edu
Office hours: Tuesday, 2 to 4, Levine 5th floor bump space -
Marco Gaboardi
gaboardi AT cs.unibo.it
Office hours: Friday, 3 to 5, Levine 5th floor bump space
Text
The main text for the course is the online book Software Foundations. A good supplemental text is Types and Programming Languages. Recommendations for some other useful books can be found in the Postscript chapter of Software Foundations.Discussion Forum
We will use Piazza for both announcements and discussions. Please register yourself there to make sure you keep up with what's happening.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, 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 7-11 | Lecture: Introduction,
functional programming Opening slides Lecture notes: Preface, Basics Homework: Basics.v (HW1) |
|
| Jan 14-18 | Lecture: Induction, Lists Opening slides Lecture notes: Induction, Lists |
Lecture: Lists, Polymorphism Lecture notes: Lists, Poly Homework: Induction.v and Lists.v (HW2) |
| Jan 21-25 | Martin Luther King, Jr. Day (no class) | Lecture: Polymorphism, functions as data, more about Coq Lecture notes: Poly | Poly.v (HW3) HW2 due at noon |
| Jan 28 - Feb 1 | Lecture: More About Coq Lecture notes: MoreCoq | MoreCoq.v | |
Lecture: Propositions and evidence Lecture notes: Prop Homework: MoreCoq.v and Prop.v (HW4) HW3 due at noon |
| Feb 4-8 | Lecture: Logic in Coq Lecture notes: MoreProp | MoreProp.v Logic | Logic.v | MoreInd | MoreInd.v |
Lecture: Logic in Coq (continued) MoreProp.v, Logic.v, and MoreInd.v (HW5) HW4 due at noon |
| Feb 11-15 | Lecture: Review Review problems |
Midterm I
(Standard version,
Advanced version,
Answers)
HW5 due at noon |
| Feb 18-22 | 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 25 - March 1 | Lecture: Program Equivalence Lecture notes: Equiv | Equiv.v |
Lecture: Program Equivalence, continued Lecture notes: Equiv | Equiv.v (HW7) HW6 due at noon |
| March 4-8 | Spring Break (no class) | Spring Break (no class) |
| March 11-15 | Lecture: Hoare Logic Lecture notes: Hoare | Hoare.v |
Lecture: Hoare Logic, continued Lecture notes: Hoare | Hoare.v (HW8) | HW7 due at noon |
| March 18-22 | Lecture: Hoare Logic, continued Lecture notes: Hoare2.v |
Lecture: Hoare Logic, continued Lecture notes: Hoare2 | Hoare2.v (HW9) | HW8 due at noon |
| March 25 - 29 | Lecture: Review Review problems |
Midterm II
(Standard version,
Advanced version,
Answers)
HW9 due at noon |
April 1-5 | Lecture: Small-Step Semantics Lecture notes: Smallstep | Smallstep.v |
Lecture: Small-Step Semantics, continued Lecture notes: Smallstep | Smallstep.v (HW10) |
| April 8-12 | Lecture: Types Lecture notes: Auto | Auto.v | Types | Types.v (HW11, part 1) | |
Lecture: Simply Typed Lambda-Calculus Lecture notes: Stlc | Stlc.v (HW11, part 2) |
| April 15-19 | Lecture: STLC, continued Lecture notes: StlcProp | StlcProp.v (HW12, part 1) | MoreStlc | MoreStlc.v (HW12, part 2) | |
Lecture: Subtyping Lecture notes: Sub | Sub.v |
| April 22 | Lecture: Subtyping, continued Lecture notes: Sub | Sub.v |
|
| Tuesday, April 30 | Final exam (9-11AM), DRLB A6 (Standard version, Standard with answers, Advanced version, Advanced with answers) |