SF

Tues, Thurs 10:30AM-noon

Moore 216

Instructor
Steve Zdancewic
stevez_NOSPAM AT cis.upenn.edu
Office hours: Weds. 3:30-5:00, Levine 511
Teaching Assistants
Jennifer Paykin
jpaykin_NOSPAM AT seas.upenn.edu
Office hours: Thurs. 3:00-4:30, 5th floor GRW Bump Space (near 562)
Dmitri Garbuzov
dmitri_NOSPAM AT seas.upenn.edu
Office hours: Mon. 4:30-6:00, 5th floor GRW Bump Space (near 562)

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.

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/27
08/29 Introduction, functional programming lec01.pdf, Preface, Basics HW1 Due 09/05:
Basics.v
09/03 Induction Induction,
09/05 Induction, Lists Induction, Lists HW2 Due 09/12: (contains "advanced" problems)
Induction.v and Lists.v
09/10 Polymorphism, functions as data Poly
09/12 More About Coq MoreCoq | MoreCoq.v HW3 Due 09/19:
Poly.v and MoreCoq.v
09/17 Logic in Coq Logic | Logic.v
09/19 Propositions and evidence Prop | Prop.v
HW4 Due 09/26:
Logic.v and Prop.v
09/24 Logic in Coq (continued) MoreLogic | MoreLogic.v
09/26 Proof Objects, Review ProofObjects | ProofObjects.v
Review problems 		HW5 Due 10/08:
MoreLogic.v and ProofObjects.v
Read: MoreInd | MoreInd.v
(MoreInd describes "informal" inductive proofs.)
10/01 Midterm I Standard Advanced Solutions
10/03 Coq automation and While programs Imp | Imp.v
ImpParser | ImpParser.v
SfLib.v
10/08 While programs (continued) HW6 Due 10/17:
Imp | Imp.v
SfLib.v (needed by Imp.v)

For your perusal, not for HW:
ImpParser | ImpParser.v
ImpCEvalFun | ImpCEvalFun.v
10/10 Fall Break - no class
10/15* Program Equivalence Equiv | Equiv.v
10/17* Program Equivalence (continued) HW7 Due 10/24:
Equiv | Equiv.v
10/22* Hoare Logic I Hoare | Hoare.v
10/24 Hoare Logic II HW8 Due 10/31:
Hoare | Hoare.v
10/29 Hoare Logic III Hoare2 | Hoare2.v
10/31 Small-Step Semantics Smallstep | Smallstep.v HW9 Due 11/8 (Friday!):
Hoare2 | Hoare2.v
11/05 Review Review problems
11/07 Midterm II Standard Advanced Solutions
11/12 Automation Auto | Auto.v
11/14 Types Types | Types.v
11/19 Simply Typed Lambda-Calculus Stlc | Stlc.v
11/21* STLC (continued) Stlc | Stlc.v StlcProp | StlcProp.v
HW10:
Smallstep | Smallstep.v
Types | Types.v
11/26 More STLC MoreStlc | MoreStlc.v
11/28 Thanksgiving Break - no class
12/03* Subtyping Sub | Sub.v HW11:
Stlc.v
StlcProp.v
MoreStlc.v
12/05* Subtyping (continued) Sub | Sub.v
12/10 Course wrap-up HW12:
Sub.v
12/13 Final exam
* indicates a date when Dr. Zdancewic will be absent.
Last modified: Wed Nov 20 11:05:57 EST 2013