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: 20%
- Midterm 1: 20%
- Midterm 2: 20%
- Final Exam: 40%
Prerequisites:
An undergraduate-level course in programming languages or compilers; significant programming experience.
Syllabus:
- Part I: Foundations
- Functional programming
- Constructive logic
- Inductive definitions and proof techniques
- The Coq proof assistant
- Part II: Basics
- Operational semantics
- The λ-calculus
- Part III: Type systems
- Simply typed λ-calculus
- Type safety
- Subtyping
- Part IV: Case study
- Featherweight Java
Textbook:
Types and Programming Languages. Benjamin C. Pierce. MIT Press, 2002.