Tuesday/Thursday: 1:45 - 3:15, ANNS 111

Benjamin Pierce
bcpierce_NOSPAM AT cis.upenn.edu
Office: Levine 562
Office hours: Mondays 2:00 - 4:00 ET
Teaching Assistants
Lef Ioannidis
elefthei_NOSPAM AT seas.upenn.edu
Office hours: Monday and Wednesday from noon to 2PM in Levine 5th floor bump space (near elevators)


The main texts for the course are the online books Logical Foundations and Programming Language Foundations, volumes 1 and 2 of the Software Foundations series. 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.

Poll Everywhere

To make lectures more interactive, we will be using the Poll Everywhere platform. There is no charge to students for using this platform.


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.

You have a total of 72 late hours to use throughout the semester, which you can divide up among the homework assignments however you like -- no need to ask or tell us. If you go over your 72 hour allocation, then any further late homeworks will incur a 25% penalty for each 24 hours (or portion thereof) after the deadline. (For example, if you turn in HW01 70 hours late, HW02 1 hour late, and HW03 2 hours late, then HW01 and HW02 will incur no penalty, while HW03 will lose 25%.)

Class Schedule

The following links provide HTML and Coq .v files for the lecture material in the course. 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. Note that the schedule is tentative.