LRSM AUD (Tues) and Levine 101 (Thus)
10:30AMnoon
 Instructor

Stephanie Weirich
sweirich AT cis.upenn.edu
Office hours: Weds, 45PM, Levine 510  Teaching Assistants

Arthur Azevedo de Amorim
aarthur AT seas.upenn.edu
Office hours: Wed 1:302:30PM, Levine 5th floor bump space 
Justin Chiu
justc AT seas.upenn.edu
Office hours: Tues 12:301:30PM, Levine 5th floor bump space
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). It is unclear whether you will be able to sell back a response card bought online at the end of the term. The Bookstore will be selling only the Response Card QT beginning Fall 2014. Any of the TurningPoint "RF" cards should work for this class, but please be aware that some other classes that you take this term or in the future might require the text functionality of the Response Card QT.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/28  Introduction, functional programming 
lec01.pdf Preface, Basics  Basics.v 
HW1 Due 09/04: Basics.v 
09/02*  Basics, Induction  Induction  
09/04*  Induction, Lists  Induction, Lists 
HW2 Due 09/11: (contains "advanced" problems) Induction.v and Lists.v 
09/09  Polymorphism, functions as data  Poly  Poly.v  
09/11  More About Coq  MoreCoq  MoreCoq.v 
HW3 Due 09/18: Poly.v and MoreCoq.v 
09/16  Logic in Coq 
Logic 
Logic.v 

09/18  Propositions and evidence 
Prop 
Prop.v 
HW4 Due 09/25: Logic.v and Prop.v 
09/23  Propositions and evidence (continued)  
09/25  Logic in Coq (continued) 
MoreLogic 
MoreLogic.v Review problems  Review1.v 
HW5 Due 10/07: MoreLogic.v Read: ProofObjects  ProofObjects.v 
09/30  Midterm I 
Fall 2013 exam: Standard  Advanced  Solutions 
Fall 2014 exam: Solutions 
10/02*  More about Induction  MoreInd 
MoreInd.v 

10/07  Coq automation and While programs 
Imp 
Imp.v 
HW6 Due 10/16: Imp.v SfLib.v (needed by Imp.v) 
10/09  Fall Break  no class  
10/14  WHILE programs (continued) 
For your perusal: ImpParser  ImpParser.v ImpCEvalFun  ImpCEvalFun.v 
Midsemester feedback survey 
10/16  Program Equivalence  Equiv  Equiv.v 
HW7 Due 10/23: Equiv.v 
10/21  Program Equivalence (continued)  
10/23  Hoare Logic I  Hoare  Hoare.v 
HW8 Due 10/30: Hoare.v 
10/28  Hoare Logic I (continued)  
10/30  Hoare Logic II  Hoare2  Hoare2.v 
HW9 Due 11/06: Hoare2.v 
11/04  Hoare Logic II (continued) and Review  Review problems  
11/06  SmallStep Semantics  Smallstep 
Smallstep.v 
HW10 Due 11/20 (Part 1): Smallstep.v 
11/11  Midterm II 
Fall 2013 exam: Standard  Advanced  Solutions 
Fall 2014 exam: Solutions 
11/13  SmallStep (continued) 
HW10 Due 11/20 (Part 2): Types.v 

11/18  Types  Types  Types.v  Read:
Auto 
Auto.v 
11/20  Simply Typed LambdaCalculus  Stlc  Stlc.v 
HW11 Due 12/2: Stlc.v and StlcProp.v 
11/25  STLC Soundness  StlcProp  StlcProp.v  NOTE: In Levine 101 (Thursday schedule) 
11/27  Thanksgiving Break  no class  
12/02  STLC Soundness (continued) and MoreStlc  MoreStlc  MoreStlc.v 
HW12 Due Sub.v 
12/04  Subtyping  Sub  Sub.v  
12/09  Subtyping (Continued)  
12/18  Final exam (911AM) DRLB A4 
Fall 2013 exam:
Advanced 
Standard 
Answers Spring 2013 exam: Advanced  Standard  Answers (Advanced)  Answers (Standard) Spring 2012 exam: Exam  Answers 