Towne 303

Tuesday/Thursday: noon-1:30

Steve Zdancewic
stevez_NOSPAM AT cis.upenn.edu
Office hours: Tuesday, 4-5PM, Levine 511 (and by appointment)
Teaching Assistants
Meyer Kizner
mkizner_NOSPAM AT seas.upenn.edu
Office hours: TBA
Matthew Weaver
mweav_NOSPAM AT sas.upenn.edu
Office hours: TBA


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 8:00PM 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 Canvas.

Tentative Schedule

The following links provide HTML and Coq .v files for the lecture material in the course. However, 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
01/14 Introduction, Functional programming in Coq lec01.pdf
Preface Basics | Basics.v
HW1 Due 01/21:
01/19 Basics, Induction Induction | Induction.v
01/21* no class
01/26* Lists Lists | Lists.v HW2 Due 01/28:
Induction.v and Lists.v
01/28 Polymorphism, functions as data Poly | Poly.v
02/02 More About Coq: Tactics Tactics | Tactics.v HW3 Due 02/04:
Poly.v and Tactics.v
02/04 Logic in Coq Logic | Logic.v
02/09 Inductive Propositions IndProp | IndProp.v
HW4 Due 02/11:
Logic.v and IndProp.v
02/11 Logic in Coq (continued) MoreLogic | MoreLogic.v
Review problems | Review1.v
02/16 Case Study: Maps HW5 Due 10/07:
Read: ProofObjects | ProofObjects.v
02/18 Midterm I Fall 2013 exam:
Standard | Advanced | Solutions
Fall 2014 exam:
02/23 WHILE programs Imp | Imp.v

HW6 Due 10/16:
SfLib.v (needed by Imp.v)
02/25 WHILE programs (continued)
For your perusal:
ImpParser | ImpParser.v
ImpCEvalFun | ImpCEvalFun.v
Midsemester feedback survey
03/01 Program Equivalence Equiv | Equiv.v HW7 Due 10/23:
03/03 Program Equivalence (continued)
03/08 Hoare Logic I Hoare | Hoare.v HW8 Due 10/30:
03/10 Spring Break - no class
03/15 Spring Break - no class
03/17 Hoare Logic I (continued)
03/22 Hoare Logic II Hoare2 | Hoare2.v HW9 Due 11/06:
03/24 Hoare Logic II (continued) Review problems
03/29 Small-Step Semantics Smallstep | Smallstep.v
HW10 Due 11/20 (Part 1):
03/31 Small-Step (continued) HW10 Due 11/20 (Part 2):
04/05 Midterm II Fall 2013 exam:
Standard | Advanced | Solutions
Fall 2014 exam:
04/07 Types Types | Types.v Read: Auto | Auto.v
04/12* Simply Typed Lambda-Calculus Stlc | Stlc.v HW11 Due 12/2:
Stlc.v and StlcProp.v
04/14* STLC Soundness StlcProp | StlcProp.v
04/19 STLC Soundness (continued) MoreStlc | MoreStlc.v HW12 Due 12/09 12/14 (hard deadline):
04/21 Subtyping Sub | Sub.v
04/26 Subtyping (Continued)
TBA Final Exam Fall 2013 exam: Advanced | Standard | Answers
Spring 2013 exam: Advanced | Standard | Answers (Advanced) | Answers (Standard)
Spring 2012 exam: Exam | Answers
* indicates a date when Dr. Zdancewic will be absent.
Last modified: Tue Feb 2 11:15:23 EST 2016