Note that the information below applies to the CIS500 course. The syllabus for the Software Foundations area of the WPE-I can be found here.

This course introduces basic concepts and techniques in the foundational study of programming languages, as well as their formal logical underpinnings. The central theme is the view of individual programs and whole languages as mathematical objects about which precise claims may be made and proved. Particular topics include operational techniques for formal definition of language features, type systems and type safety properties, polymorphism and subtyping, and foundations of object-oriented programming.


Breakdown for the course grade is as follows:

Advanced/WPE Track

CIS 500 can be taken in one of two tracks: regular and advanced. The difference is that the advanced track features more and harder exercises; it also has more challenging exams.

  • Students (Ph.D. in particular) wishing to take CIS 500 for WPE I credit must follow the advanced track.
  • All students start in the "advanced" status by default.
  • Students may switch from "advanced" to "regular" status at any time by notifying the course staff, after which they remain on "regular" status for the rest of the course (except as described below).
  • Any student wishing to switch from "regular" to "advanced" status must make up all missing "advanced" exercises before the first midterm. After the first midterm exam, no switching from regular to advanced is allowed.
  • Only students taking the course in the "advanced" track are eligible to receive an A+.


Homework can be submitted via Canvas. If you are taking the course but cannot access the CIS 500 Canvas, 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 at 8:00pm on the due date. 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).


An undergraduate-level course in programming languages or compilers; significant programming experience; mathematical sophistication.


Part I: Foundations
Functional programming
Constructive logic
Inductive definitions and proof techniques for informal and formal proof
The Coq proof assistant
Part II: Basics
Operational semantics
Semantics of the imperative While language
Part III: Type systems
Simply typed λ-calculus
Type safety
Dependently typed programming


Online textbook: Software Foundations

Supplementary textbook: Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.

Last modified: Sun Sep 1 10:43:56 EDT 2013