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  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: MoreLogic.v Read: ProofObjects  ProofObjects.v 

02/18  Midterm I 
Fall 2013 exam: Standard  Advanced  Solutions 
Fall 2014 exam: Solutions 
02/23  WHILE programs 
Imp 
Imp.v 
HW6 Due 10/16: Imp.v 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: Equiv.v 
03/03  Program Equivalence (continued)  
03/08  Hoare Logic I  Hoare  Hoare.v 
HW8 Due 10/30: Hoare.v 
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: Hoare2.v 
03/24  Hoare Logic II (continued)  Review problems  
03/29  SmallStep Semantics  Smallstep 
Smallstep.v 
HW10 Due 11/20 (Part 1): Smallstep.v 
03/31  SmallStep (continued) 
HW10 Due 11/20 (Part 2): Types.v 

04/05  Midterm II 
Fall 2013 exam: Standard  Advanced  Solutions 
Fall 2014 exam: Solutions 
04/07  Types  Types  Types.v  Read:
Auto 
Auto.v 
04/12*  Simply Typed LambdaCalculus  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 Sub.v 
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 