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.
Grading:
Breakdown for the course grade is as follows:
- Homework: 25%
- Midterm 1: 20%
- Midterm 2: 20%
- Final Exam: 35%
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.
- Only students taking the course in the "advanced" track are eligible to receive an A+.
- All students start in the "advanced" track 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.
- Students intending to take the CIS 500 WPE I exam are strongly recommended to follow the advanced track.
Prerequisites:
An undergraduate-level course in programming languages or compilers; significant programming experience; mathematical sophistication.
Syllabus:
- 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
- Subtyping
Textbook:
Online textbooks: Logical Foundations and Programming Language Foundations
Supplementary textbook: Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.