Towne 303
Tuesday/Thursday: noon1:30
 Instructor

Steve Zdancewic
stevez AT cis.upenn.edu
Office hours: Tuesday, 45PM, Levine 511 (and by appointment)  Teaching Assistants

Meyer Kizner
mkizner AT seas.upenn.edu
Office hours: TBA 
Matthew Weaver
mweav AT sas.upenn.edu
Office hours: TBA
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 inclass 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 casesensitive).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: Basics.v 
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  Logic in Coq (Continued) 
HW4 Due 02/11: Logic.v 

02/11  Inductive Propositions 
IndProp 
IndProp.v 

02/16  Inductive Propositions 
HW5 Due 02/18: IndProp.v and Maps.v 

02/18  Case Study: Maps  Maps  Maps.v  
02/23  Midterm I 
SOLUTIONS Fall 2014 exam: Standard  Advanced  Solutions Fall 2013 exam: Standard  Advanced  Solutions 

02/25  WHILE programs 
SfLib 
SfLib.v Imp  Imp.v For your perusal: ImpParser  ImpParser.v ImpCEvalFun  ImpCEvalFun.v 

03/01  Program Equivalence  Equiv  Equiv.v 
HW6 Due 3/3: Imp.v 
03/03  Program Equivalence (continued)  
03/08  Spring Break  no class  
03/10  Spring Break  no class  
03/15  Hoare Logic I  Hoare  Hoare.v 
HW7 Due 3/17: Equiv.v 
03/17  Hoare Logic (continued)  
03/22  Hoare Logic (continued)  Hoare2  Hoare2.v  
03/24  SmallStep Semantics  Smallstep 
Smallstep.v 

03/29  SmallStep Semantics (continued) 
HW08 Due 03/31: Hoare.v and Hoare2.v 

03/31  Types  Types  Types.v  
04/05  Simply Typed LambdaCalculus  Stlc  Stlc.v  HW09 Due: 04/05 Smallstep.v 
04/07  Midterm II 
SOLUTIONS Fall 2013 exam: Standard  Advanced  Solutions Fall 2014 exam: Standard  Advanced  Solutions 
Read:
Auto 
Auto.v 
04/12*  STLC Soundness  StlcProp  StlcProp.v 
HW10 Due 4/14: Types.v 
04/14*  STLC Soundness (continued)  StlcProp  StlcProp.v  
04/19  More STLC  MoreStlc  MoreStlc.v 
HW11 Due 4/21: Stlc.v and StlcProp.v 
04/21  Subtyping  Sub  Sub.v  
04/26  Subtyping (Continued) 
HW12 Due 4/27: Sub.v 

5/3  Final Exam 
Fall 2013 exam:
Advanced 
Standard 
Answers Spring 2013 exam: Advanced  Standard  Answers (Advanced)  Answers (Standard) 