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