Berger Auditorium (basement floor of Skirkanich Hall)
Tuesday/Thursday: noon1:30
 Instructor

Benjamin Pierce
bcpierce AT cis.upenn.edu
Office: Levine 562
Office hours: Tuesdays, 45:30  Teaching Assistants

Kenny Foner
kfoner AT seas.upenn.edu
Office hours: Fridays 10AMnoon (near Levine 5th floor elevator) 
Christine Rizkallah
criz AT seas.upenn.edu
Office hours: Thursdays 46PM (near Levine 5th floor elevator) 
Antoine Voizard
voizard AT seas.upenn.edu
Office hours: Mondays 24PM (near Levine 5th floor elevator)
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 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 2448 hours, and 75% for 4872 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: Basics.v 

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: Logic.v 

09/22  Logic in Coq  Logic  
09/27  Inductively defined propositions  IndProp 
HW5 Due 10/4: IndProp.v 

09/29  Inductively defined propositions, proof objects  IndProp, ProofObjects  
10/4 (Tue), in class  Midterm I 
Study materials (newer ones are
best aligned with current coverage of material, but older ones
are worth looking at) Exam (with solutions) 

10/11  Total and partial maps, modeling an imperative programming language  Maps, Imp (and optionally ImpParser and ImpCEvalFun) 
HW6 Due 10/18: Maps.v, Imp.v (you may also want to play with ImpParser.v and ImpCEvalFun.v) 

10/13  More automation  Auto  (you may also want to play with Auto.v)  
10/18  Program equivalence  Equiv 
HW7 Due 10/25: Equiv.v 

10/20  Program equivalence (continued)  
10/25  Hoare Logic  Hoare 
HW8 Due 11/1: Hoare.v, Hoare2.v 

10/27  Hoare Logic (continued)  Hoare2  
11/1  Smallstep operational semantics  Smallstep 
HW9 Due 11/8: Smallstep.v 

11/3  (continued)  
11/8  Midterm II 
Study materials (newer ones are
best aligned with current coverage of material, but older ones
are worth looking at) Exam (with solutions) 

11/10  A First Taste of Types  Types 
HW10 Due 11/15: Types.v 

11/15  Simply Typed Lambda Calculus  Stlc 
HW11 Due 11/29: (part 1) Stlc.v 

11/17  Properties of the STLC  StlcProp  (HW11, part 2) StlcProp.v  
11/21  Extending the STLC  MoreStlc  
11/29  Extending the STLC, continued  MoreStlc 
HW12 Due 12/6: (part 1) MoreStlc.v 

12/1  Typechecking, subtyping  Typechecking  HW12, (part 2): Typechecking.v  
12/20 (Tue), noon2PM  Final Exam 