Type Systems for Programming Languages
Author :
Robert Harper,
Computer Science Department,
Carnegie Mellon University
Pages : 199
Working Draft : Spring 2000
Terms and Conditions:
| Robert Harper wrote: |
| These are course notes Computer Science 15–814 at Carnegie Mellon University. This is an incomplete, working draft, not intended for publication. Citations to the literature are spotty at best; no results presented here should be considered original unless explicitly stated otherwise. Please do not distribute these notes without the permission of the author. |
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
