Tuesday/Thursday: noon-1:30
- Instructor
-
Benjamin Pierce
bcpierce AT cis.upenn.edu
Office: Levine 562
Office hours: Mondays 1:30 - 3:30 ET - Teaching Assistants
-
Lucas Silver
lucsil AT seas.upenn.edu
Office hours: Tuesdays 3:00 PM - 5:00 PM ET (through 11/11) -
Irene Yoon
euisuny AT cis.upenn.edu
Office hours: Mondays 5:00pm - 7:00pm ET
Text
The main texts for the course are the online books Logical Foundations and Programming Language Foundations, volumes 1 and 2 of the Software Foundations series. 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.Poll Everywhere
To make lectures more interactive, we will be using the Poll Everywhere platform. There is no charge to students for using this platform.Homework
Homework can be submitted via Canvas. If you are taking the course but cannot access the CIS 500 Canvas pages, 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 normally due at 11:30AM on the date specified (exceptions noted below). Late homework submissions will be accepted for up to three days, with a 25% reduction in credit per late day (25% for up to 24 hours late, 50% for 24-48 hours, and 75% for 48-72 hours). Solutions will be posted on Canvas.
Class Schedule
The following links provide HTML and Coq .v files for the lecture material in the course. These materials will be updated throughout the semester, so please be sure that you use the most recent version of the files, especially for homework. Note that the schedule is tentative.
| Date | Topics | Reading | Homework Due (normally Tuesdays at 11:30AM) |
| 9/1 | Introduction, functional programming in Coq | Intro slides, Preface (Preface.v), Basics (Basics.v) | |
| 9/3 | Basics (continued) | ||
| 9/8 | Induction, data structures | Induction (Induction.v), Lists (Lists.v) | HW1: Basics.v BasicsTest.v Preface.v |
| 9/10 | Polymorphism, functions as data | Lists (Lists.v), Poly (Poly.v) | |
| 9/15 | More basic tactics | Tactics (Tactics.v) | HW2: Induction.v InductionTest.v Lists.v ListsTest.v _CoqProject |
| 9/17 | More basic tactics (continued) | Tactics (Tactics.v), Logic (Logic.v) | |
| 9/22 | Logic in Coq | Logic (Logic.v) | HW3: Poly.v PolyTest.v Tactics.v TacticsTest.v |
| 9/24 | Logic in Coq | Logic (Logic.v) | |
| 9/29 | Inductively defined propositions | IndProp (IndProp.v) | HW4: Logic.v LogicTest.v |
| 10/1 | Inductively defined propositions, proof objects | IndProp (IndProp.v), ProofObjects (ProofObjects.v) | |
| 10/6 | Total and partial maps; modeling an imperative programming language | Maps (Maps.v), Imp (Imp.v), ImpParser (ImpParser.v), ImpCEvalFun (ImpCEvalFun.v) | HW5: IndProp.v IndPropTest.v |
| 10/8 | Midterm I (covering up to IndProp chapter) | Past exams, Exam with solutions | |
| 10/13 | More automation | Auto (Auto.v) | |
| 10/15 | No class ('Fall break') | ||
| 10/20 | Program equivalence | Equiv (Equiv.v) | HW6: Maps.v MapsTest.v Imp.v ImpTest.v (you may also want to play with ImpParser.v , ImpCEvalFun.v , and Auto.v ) |
| 10/22 | Program equivalence (continued) | ||
| 10/27 | Hoare Logic | Hoare (Hoare.v) | |
| 10/29 | Hoare Logic (continued) | Hoare2 (Hoare2.v) | HW7: Equiv.v EquivTest.v (you will need fresh copies of _CoqProject , Maps.v , and Imp.v ; also please read Auto.v ) |
| 11/3 | No class (Election day) | ||
| 11/5 | Small-step operational semantics | Smallstep (Smallstep.v) | HW8: Hoare.v HoareTest.v Hoare2.v Hoare2Test.v |
| 11/10 | A First Taste of Types | Types (Types.v) | |
| 11/12 | Simply Typed Lambda Calculus | Stlc (Stlc.v) | HW9: Smallstep.v SmallstepTest.v |
| 11/17 | Midterm II (covering up to Smallstep chapter) | Exam, Exam with solutions, Past exams | |
| 11/19 | STLC, continued; Properties of the STLC | StlcProp (StlcProp.v) | |
| 11/24 | Properties of the STLC, continued | HW10: Types.v TypesTest.v | |
| 11/26 | No class (Thanksgiving) | ||
| 12/1 | Extending the STLC | MoreStlc (MoreStlc.v), Typechecking (Typechecking.v) | |
| 12/3 | Subtyping | Sub (Sub.v) | HW11: Stlc.v StlcTest.v StlcProp.v StlcPropTest.v |
| 12/8 | Subtyping | Sub (Sub.v) | |
| 12/10 | no class (Monday schedule) | HW12: MoreStlc.v MoreStlcTest.v Typechecking.v TypecheckingTest.v | |
| 12/16 | Final Exam - Dec 16 (9AM EST) to 18 (9AM EST) | Past exams , exam, solutions |