Berger Auditorium (Skirkanich Hall)

Tuesday/Thursday: noon-1:30

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)


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.


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:
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:
09/22 Logic in Coq Logic
09/27 Inductively defined propositions IndProp HW5 Due 09/28:
IndProp.v (again, feel free to get started looking at the exercises chapter, but remember to re-download the final version on Thursday after 2PM and copy over your solutions...)
10/4 (Tue), in class Midterm I Study materials (newer ones are better aligned with current coverage of material and probably more useful)
10/8 (Tue), in class Midterm II (tentative)
12/20 (Tue), noon-2PM Final Exam