SF

Towne 303

Tuesday/Thursday: noon-1:30

Instructor
Steve Zdancewic
stevez_NOSPAM AT cis.upenn.edu
Office hours: Tuesday, 4-5PM, Levine 511 (and by appointment)
Teaching Assistants
Meyer Kizner
mkizner_NOSPAM AT seas.upenn.edu
Office hours: TBA
Matthew Weaver
mweav_NOSPAM 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 in-class 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 case-sensitive).

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 Small-Step Semantics Smallstep | Smallstep.v
03/29 Small-Step Semantics (continued) HW08 Due 03/31:
Hoare.v and Hoare2.v
03/31 Types Types | Types.v
04/05 Simply Typed Lambda-Calculus 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 SOLUTIONS
Fall 2013 exam: Advanced | Standard | Answers
Spring 2013 exam: Advanced | Standard | Answers (Advanced) | Answers (Standard)
* indicates a date when Dr. Zdancewic will be absent.
Last modified: Wed May 11 15:55:37 EDT 2016