SF

Berger Auditorium (basement floor of Skirkanich Hall)

Tuesday/Thursday: noon-1:30

Instructor
Benjamin Pierce
bcpierce_NOSPAM AT cis.upenn.edu
Office: Levine 562
Office hours: Tuesdays, 4-5:30
Teaching Assistants
Kenny Foner
kfoner_NOSPAM AT seas.upenn.edu
Office hours: Fridays 10AM-noon (near Levine 5th floor elevator)
Christine Rizkallah
criz_NOSPAM AT seas.upenn.edu
Office hours: Thursdays 4-6PM (near Levine 5th floor elevator)
Antoine Voizard
voizard_NOSPAM AT seas.upenn.edu
Office hours: Mondays 2-4PM (near Levine 5th floor elevator)

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.

Clickers

Students are required to buy a Turning Point "clicker" for in-class participation. These will be available in the Bookstore and can be sold back at the end of the semester for a substantial fraction of the original purchase price. The clickers can also be bought online by going to Turning Technologies and entering Penn's school code Bg2Y (this code is case-sensitive).

Homework submission

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 due at 11:00AM 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 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.

Date Topic Notes Homework
08/30 Introduction, Functional programming in Coq Intro slides,
Preface, Basics 		HW1 Due 09/06:
Basics.v
09/01 Basics, Induction Induction
09/06 Induction, simple data structures Induction, Lists HW2 Due 09/13:
Induction.v, Lists.v
09/08 Lists, polymorphism Lists, Poly
01/13 Polymorphism, functions as data Poly HW3 Due 09/20:
Poly.v, Tactics.v
01/15 More Basic Tactics Tactics
09/20 Logic in Coq Logic HW4 Due 09/27:
Logic.v
09/22 Logic in Coq Logic
09/27 Inductively defined propositions IndProp HW5 Due 10/4:
IndProp.v
09/29 Inductively defined propositions, proof objects IndProp, ProofObjects
10/4 (Tue), in class Midterm I Study materials (newer ones are best aligned with current coverage of material, but older ones are worth looking at)
Exam (with solutions)
10/11 Total and partial maps, modeling an imperative programming language Maps, Imp (and optionally ImpParser and ImpCEvalFun) HW6 Due 10/18:
Maps.v, Imp.v (you may also want to play with ImpParser.v and ImpCEvalFun.v)
10/13 More automation Auto (you may also want to play with Auto.v)
10/18 Program equivalence Equiv HW7 Due 10/25:
Equiv.v
10/20 Program equivalence (continued)
10/25 Hoare Logic Hoare HW8 Due 11/1:
Hoare.v, Hoare2.v
10/27 Hoare Logic (continued) Hoare2
11/1 Small-step operational semantics Smallstep HW9 Due 11/8:
Smallstep.v
11/3 (continued)
11/8 Midterm II Study materials (newer ones are best aligned with current coverage of material, but older ones are worth looking at)
Exam (with solutions)
11/10 A First Taste of Types Types HW10 Due 11/15:
Types.v
11/15 Simply Typed Lambda Calculus Stlc HW11 Due 11/29:
(part 1) Stlc.v
11/17 Properties of the STLC StlcProp (HW11, part 2) StlcProp.v
11/21 Extending the STLC MoreStlc
11/29 Extending the STLC, continued MoreStlc HW12 Due 12/6:
(part 1) MoreStlc.v
12/1 Typechecking, subtyping Typechecking HW12, (part 2): Typechecking.v
12/6 Subtyping Sub HW13 Due 12/18 at 11:59PM: Sub.v
12/20 (Tue), noon-2PM, in DRLB A4 Final Exam Past exams Exam (with solutions)