"These notes were prepared for use in the graduate course Computer Science 15–
814: Type Systems for Programming Languages at Carnegie Mellon University.
Their purpose is to provide a unified account of the role of type theory in
programming language design and implementation. The stress is on the use of
types as a tool for analyzing programming language features and studying their
implementation."