Type Systems for Programming Languages
These lecture notes provides 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.
Tag(s): Functional Programming
Publication date: 01 Jan 2000
ISBN-10: n/a
ISBN-13: n/a
Paperback: 199 pages
Views: 17,433
Type: Lecture Notes
Publisher: n/a
License: n/a
Post time: 06 Nov 2006 08:57:15
Type Systems for Programming Languages
These lecture notes provides 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.
Publication date: 01 Jan 2000
ISBN-10: n/a
ISBN-13: n/a
Paperback: 199 pages
Views: 17,433
Document Type: Lecture Notes
Publisher: n/a
License: n/a
Post time: 06 Nov 2006 08:57:15
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.
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.
Tweet
About The Author(s)
Robert "Bob" William Harper, Jr. is a professor in the Computer Science Department at the Carnegie Mellon University. His research interest is mathematical principles of programming. He made major contributions to the design of the Standard ML programming language and the LF logical framework.
Robert "Bob" William Harper, Jr. is a professor in the Computer Science Department at the Carnegie Mellon University. His research interest is mathematical principles of programming. He made major contributions to the design of the Standard ML programming language and the LF logical framework.