Types and Programming Languages

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:

  1. Introduction
  2. Mathematical Preliminaries (sets, induction, etc.)
  3. Untyped lambda calculus and operational semantics
  4. Simply-typed lambda calculus and type systems
  5. Type safety proofs
  6. Subtyping
  7. Featherweight Java
  8. Gradual type systems that mix static and dynamic typing
  9. Polymorphism: universal and existential types
  10. Type inference and ML
  11. Bounded quantification
  12. C++ constrained templates
  13. Higher-order type systems with type operators
  14. 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.

  1. HW 1 Due Tuesday, Jan. 29. solution
  2. HW 2 Due Tuesday, Feb. 5.
  3. HW 3 Due Tuesday, Feb. 26.
  4. HW 4 Due Tuesday, May 6.

Reading:

  1. TAPL Chapters 1, 2 (by Jan. 22)
  2. TAPL Chapters 3, 4, 5, 6 (by Jan. 29) (Optional Isa Ch 1, 2)
  3. TAPL Chapters 7, 8, 9, 10 (by Feb. 5)
  4. Chapters 11, 12, 13, 14 (by Feb. 12)
  5. Chapters 15, 16, 17 (by Feb. 19)
  6. Chapters 18, 19, 20, 21 (by Feb. 26)
  7. Chapters 22, 23, 24, 25 (by Mar. 4)

Class Email Group

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