CIS 500: Software Foundations - Spring 2010

Picture of TAPL

Mon, Wed 3:00-4:30PM

Towne 303

Benjamin C. Pierce
bcpierce_NOSPAM AT
office hours: by appointment
Teaching Assistants
Vilhelm Sjöberg
vilhelm_NOSPAM AT
office hours: Tuesdays, 4-6 in Moore 207
Brent Yorgey
byorgey_NOSPAM AT
office hours: Mondays, 5-7 in Moore 100A


The main text for the course is the online book Software Foundations. Recommendations for some useful supplemental texts can be found in the preface.

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, please 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 before class. 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.


Week Monday Wednesday
Jan 11-15 Lecture: Introduction, functional programming (numbers, lists), basic proofs
Introductory slides
Lecture notes: Preface, Basics | Basics.v (HW1)
Jan 18-22 Martin Luther King, Jr. Day (no class) Lecture: Lists
Lecture notes: Lists | Lists.v (HW2)
HW1 due
Jan 25-29 Lecture: Polymorphism, functions as data
Lecture notes: Poly | Poly.v
Lecture: More About Coq
Lecture notes: Poly | Poly.v (HW3)
HW2 due
Feb 1-5 Lecture: Propositions and evidence
Lecture notes: Ind | Ind.v
Lecture: Propositions and evidence (continued)
Lecture notes: Ind | Ind.v (HW4)
HW3 due
Feb 8-12 Lecture: Logic in Coq
Lecture notes: Logic | Logic.v
Lecture: cancelled due to weather
Logic.v (HW5)
HW4 due
Feb 15-19 Lecture: Review
Lecture notes: Template for informal proofs
Midterm I (exam, solutions)
HW5 due
Feb 22-26 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) | ImpParser | ImpParser.v | SfLib.v
March 1-5 Lecture: Program Equivalence
Lecture notes: Equiv | Equiv.v
Lecture: Program Equivalence, continued
Lecture notes: Equiv | Equiv.v (HW7)
March 15-19 Lecture: Hoare Logic
Lecture notes: Hoare | Hoare.v
Lecture: Hoare Logic, continued
Lecture notes: Hoare | Hoare.v (HW8) | MoreHoare | MoreHoare.v (HW8)
March 22-26 Lecture: Small-Step Semantics
Lecture notes: Rel | Rel.v | Smallstep | Smallstep.v
You'll also need updated versions of SfLib.v and Imp.v
Lecture: Small-Step Semantics, continued
Lecture notes: Smallstep | Smallstep.v (HW9)
For the HW, you'll also need updated versions of SfLib.v and Imp.v
March 29 - April 2 Review Midterm II (exam, solutions)
April 5-9 Lecture: Simply Typed Lambda-Calculus
Lecture notes: Stlc | Stlc.v |
Lecture: STLC, continued
Lecture notes: Stlc | Stlc.v (HW10)
April 12-14 Lecture: STLC, Continued
Lecture notes: MoreStlc | MoreStlc.v |
Lecture: STLC, References
Lecture notes: MoreStlc | MoreStlc.v (HW11) | References | References.v
April 19-21 Lecture: References, continued
Lecture notes: References | References.v
Lecture: References; Subtyping
Lecture notes: References | References.v (HW12, part 1)
Subtyping | Subtyping.v (HW12, part 2)
April 26 Lecture: Subtyping, continued
Lecture notes: Subtyping | Subtyping.v
May 3 Final: exam, answers