Type Systems for Programming Languages

Author : Robert Harper, Computer Science Department, Carnegie Mellon University
Pages : 199
Working Draft : Spring 2000

Terms and Conditions:


Draft Excerpts:

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.

The course studies the theory of type systems, with a focus on applications of type systems to practical programming languages. The emphasis is on the mathematical foundations underlying type systems and operational semantics. The course includes a broad survey of the components that make up existing type systems, and also teaches the methodology behind the design of new type systems.

A number of excellent books and articles are available as background reading for this course. Of particular relevance are Proofs and Types by Jean-Yves Girard, Intuitionistic Type Theory by Per Martin-Löf, Semantics of Programming Languages by Carl Gunter, and The Formal Semantics of Programming Languages by Glynn Winskel. Other sources are mentioned at the end of each chapter, but no attempt is made to provide a comprehensive list of sources.

View/Download Type Systems for Programming Languages | Course webpage