CIS 500: Software Foundations - Spring 2013


Mon, Wed 3:00-4:30PM

Moore 216

Benjamin C. Pierce
bcpierce_NOSPAM AT
Office hours: Monday 4:30 to 6, Levine 562
Teaching Assistants
Arthur Azevedo de Amorim
aarthur_NOSPAM AT
Office hours: Tuesday, 2 to 4, Levine 5th floor bump space
Marco Gaboardi
gaboardi_NOSPAM AT
Office hours: Friday, 3 to 5, Levine 5th floor bump space


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 Blackboard. If you are taking the course but cannot access the CIS 500 Blackboard, 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 noon 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 Blackboard.

Tentative Schedule

Week Monday Wednesday
Jan 7-11 Lecture: Introduction, functional programming
Opening slides
Lecture notes: Preface, Basics
Homework: Basics.v (HW1)
Jan 14-18 Lecture: Induction, Lists
Opening slides
Lecture notes: Induction, Lists
Lecture: Lists, Polymorphism
Lecture notes: Lists, Poly
Homework: Induction.v and Lists.v (HW2)
Jan 21-25 Martin Luther King, Jr. Day (no class) Lecture: Polymorphism, functions as data, more about Coq
Lecture notes: Poly | Poly.v (HW3)
HW2 due at noon
Jan 28 - Feb 1 Lecture: More About Coq
Lecture notes: MoreCoq | MoreCoq.v |
Lecture: Propositions and evidence
Lecture notes: Prop
Homework: MoreCoq.v and Prop.v (HW4)
HW3 due at noon
Feb 4-8 Lecture: Logic in Coq
Lecture notes: MoreProp | MoreProp.v Logic | Logic.v | MoreInd | MoreInd.v
Lecture: Logic in Coq (continued)
MoreProp.v, Logic.v, and MoreInd.v (HW5)
HW4 due at noon
Feb 11-15 Lecture: Review
Review problems
Midterm I (Standard version, Advanced version, Answers)
HW5 due at noon
Feb 18-22 Lecture: Coq automation and while programs
Lecture notes: Imp | Imp.v | ImpParser | ImpParser.v | SfLib.v
Lecture: While programs
Lecture notes: Imp | Imp.v (HW6) | SfLib.v (needed for HW6)
Supplementary files: ImpParser | ImpParser.v | ImpCEvalFun | ImpCEvalFun.v
Feb 25 - March 1 Lecture: Program Equivalence
Lecture notes: Equiv | Equiv.v
Lecture: Program Equivalence, continued
Lecture notes: Equiv | Equiv.v (HW7)
HW6 due at noon
March 4-8 Spring Break (no class) Spring Break (no class)
March 11-15 Lecture: Hoare Logic
Lecture notes: Hoare | Hoare.v
Lecture: Hoare Logic, continued
Lecture notes: Hoare | Hoare.v (HW8) |
HW7 due at noon
March 18-22 Lecture: Hoare Logic, continued
Lecture notes: Hoare2.v
Lecture: Hoare Logic, continued
Lecture notes: Hoare2 | Hoare2.v (HW9) |
HW8 due at noon
March 25 - 29 Lecture: Review
Review problems
Midterm II (Standard version, Advanced version, Answers)
HW9 due at noon
April 1-5 Lecture: Small-Step Semantics
Lecture notes: Smallstep | Smallstep.v
Lecture: Small-Step Semantics, continued
Lecture notes: Smallstep | Smallstep.v (HW10)
April 8-12 Lecture: Types
Lecture notes: Auto | Auto.v | Types | Types.v (HW11, part 1) |
Lecture: Simply Typed Lambda-Calculus
Lecture notes: Stlc | Stlc.v (HW11, part 2)
April 15-19 Lecture: STLC, continued
Lecture notes: StlcProp | StlcProp.v (HW12, part 1) | MoreStlc | MoreStlc.v (HW12, part 2) |
Lecture: Subtyping
Lecture notes: Sub | Sub.v
April 22 Lecture: Subtyping, continued
Lecture notes: Sub | Sub.v
Tuesday, April 30 Final exam (9-11AM), DRLB A6
(Standard version, Standard with answers, Advanced version, Advanced with answers)