Tues, Thurs 10:30AMnoon
Moore 216
 Instructor

Steve Zdancewic
stevez AT cis.upenn.edu
Office hours: Weds. 3:305:00, Levine 511  Teaching Assistants

Jennifer Paykin
jpaykin AT seas.upenn.edu
Office hours: Thurs. 3:004:30, 5th floor GRW Bump Space (near 562) 
Dmitri Garbuzov
dmitri AT seas.upenn.edu
Office hours: Mon. 4:306:00, 5th floor GRW Bump Space (near 562)
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 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 

08/27  
08/29  Introduction, functional programming  lec01.pdf, Preface, Basics 
HW1 Due 09/05: Basics.v 
09/03  Induction  Induction,  
09/05  Induction, Lists  Induction, Lists 
HW2 Due 09/12: (contains "advanced" problems) Induction.v and Lists.v 
09/10  Polymorphism, functions as data  Poly  
09/12  More About Coq  MoreCoq  MoreCoq.v 
HW3 Due 09/19: Poly.v and MoreCoq.v 
09/17  Logic in Coq 
Logic 
Logic.v 

09/19  Propositions and evidence 
Prop 
Prop.v 
HW4 Due 09/26: Logic.v and Prop.v 
09/24  Logic in Coq (continued) 
MoreLogic 
MoreLogic.v 

09/26  Proof Objects, Review 
ProofObjects 
ProofObjects.v Review problems 
HW5 Due 10/08: MoreLogic.v and ProofObjects.v Read: MoreInd  MoreInd.v (MoreInd describes "informal" inductive proofs.) 
10/01  Midterm I  Standard Advanced Solutions  
10/03  Coq automation and While programs 
Imp 
Imp.v ImpParser  ImpParser.v SfLib.v 

10/08  While programs (continued) 
HW6 Due 10/17: Imp  Imp.v SfLib.v (needed by Imp.v) For your perusal, not for HW: ImpParser  ImpParser.v ImpCEvalFun  ImpCEvalFun.v 

10/10  Fall Break  no class  
10/15*  Program Equivalence  Equiv  Equiv.v  
10/17*  Program Equivalence (continued) 
HW7 Due 10/24: Equiv  Equiv.v 

10/22*  Hoare Logic I  Hoare  Hoare.v  
10/24  Hoare Logic II 
HW8 Due 10/31: Hoare  Hoare.v 

10/29  Hoare Logic III  Hoare2  Hoare2.v  
10/31  SmallStep Semantics  Smallstep  Smallstep.v 
HW9 Due 11/8 (Friday!): Hoare2  Hoare2.v 
11/05  Review  Review problems  
11/07  Midterm II  Standard Advanced Solutions  
11/12  Automation 
Auto 
Auto.v 

11/14  Types  Types  Types.v  
11/19  Simply Typed LambdaCalculus  Stlc  Stlc.v  
11/21*  STLC (continued) 
Stlc 
Stlc.v
StlcProp 
StlcProp.v 
HW10: Smallstep  Smallstep.v Types  Types.v 
11/26  More STLC  MoreStlc  MoreStlc.v  
11/28  Thanksgiving Break  no class  
12/03*  Subtyping  Sub  Sub.v  HW11: Stlc.v StlcProp.v MoreStlc.v 
12/05*  Subtyping (continued)  Sub  Sub.v  
12/10  Course wrapup 
HW12: Sub.v 

12/13  Final exam 