SF

LRSM AUD (Tues) and Levine 101 (Thus)

10:30AM-noon

Instructor
Stephanie Weirich
sweirich_NOSPAM AT cis.upenn.edu
Office hours: Weds, 4-5PM, Levine 510
Teaching Assistants
Arthur Azevedo de Amorim
aarthur_NOSPAM AT seas.upenn.edu
Office hours: Wed 1:30-2:30PM, Levine 5th floor bump space
Justin Chiu
justc_NOSPAM AT seas.upenn.edu
Office hours: Tues 12:30-1: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 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). 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 Small-Step 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 Small-Step (continued) HW10 Due 11/20 (Part 2):
Types.v
11/18 Types Types | Types.v Read: Auto | Auto.v
11/20 Simply Typed Lambda-Calculus 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 12/09 12/14 (hard deadline):
Sub.v
12/04 Subtyping Sub | Sub.v
12/09 Subtyping (Continued)
12/18 Final exam (9-11AM)
DRLB A4
Fall 2013 exam: Advanced | Standard | Answers
Spring 2013 exam: Advanced | Standard | Answers (Advanced) | Answers (Standard)
Spring 2012 exam: Exam | Answers
* indicates a date when Dr. Weirich will be absent.
Last modified: Fri Dec 12 09:51:11 EST 2014