Frustrated with your current programming language? Ever wanted to create your own? This course teaches you the state of the art tools and techniques for defining programming languages and proving that they do what you want them to do. You will learn about type systems and operational semantics and how to use them to model modern programming language features such as objects and generics. You will come away knowing the fundamental principles common to most programming languages, making it much easier to learn new languages.
When: Spring 2008
Where: ECCR 137
Textbook: Types and Programming Languages by Benjamin C. Pierce
Optional textbook:: Isabelle/HOL: A Proof Assistant for Higher-Order Logic
Class times: 2:00-3:15pm Tuesday & Thursday
Office hours: 1:00-2:00pm Tuesday
Course outline:
- Introduction
- Mathematical Preliminaries (sets, induction, etc.)
- Untyped lambda calculus and operational semantics
- Simply-typed lambda calculus and type systems
- Type safety proofs
- Subtyping
- Featherweight Java
- Gradual type systems that mix static and dynamic typing
- Polymorphism: universal and existential types
- Type inference and ML
- Bounded quantification
- C++ constrained templates
- Higher-order type systems with type operators
- Type systems for metaprogramming and MetaML
Assignments: There will be weekly homework from questions in the book and four programming assignments that develop type checkers and interpreters for the languages studied in the course.
- HW 1 Due Tuesday, Jan. 29. solution
- HW 2 Due Tuesday, Feb. 5.
- HW 3 Due Tuesday, Feb. 26.
- HW 4 Due Tuesday, May 6.
Reading:
- TAPL Chapters 1, 2 (by Jan. 22)
- TAPL Chapters 3, 4, 5, 6 (by Jan. 29) (Optional Isa Ch 1, 2)
- TAPL Chapters 7, 8, 9, 10 (by Feb. 5)
- Chapters 11, 12, 13, 14 (by Feb. 12)
- Chapters 15, 16, 17 (by Feb. 19)
- Chapters 18, 19, 20, 21 (by Feb. 26)
- Chapters 22, 23, 24, 25 (by Mar. 4)
Exams: There will be a midterm and final exam.
The midterm is take-home and due March 4.
Lectures:
- Lecture 2: Inductive sets, recursive functions, proof by rule induction pdf
- Lecture 3: Small-step, Lambda Calculus, Substitution, Evaluation Contexts pdf
- Lecture 4: Big-step, DeBruijn, Locally nameless pdf
- Lecture 5: Virtual and Abstract Machines pdf
- Lecture 6: Simple Types and Type Safety pdf
- Lecture 7: More Type Safety, STLC pdf
- Lecture 8: Extensions to the STLC pdf
- Lecture 9: References, Exceptions, Normalization pdf
- Lecture 10: Subtyping pdf
- Lecture 11: More Subtyping pdf
- Lecture 12: Encoding Objects pdf
- Lecture 13: Featherweight Java pdf
- Lecture 14: Gradual Typing
- Lecture 15: Recursive Types pdf
- Lecture 16: Generics (parametric polymorphism) and System Fpdf
- Lecture 17: Existential Types pdf
- Lecture 18: Type Inference pdf
- Lecture 19: Correctness of Unification pdf