**Type Systems for Programming Languages**

by Robert Harper

2000**Number of pages**: 199

**Description**:

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.

Download or read it online for free here:

**Download link**

(0.8MB, PDF)

## Similar books

**Semantics: Advances in Theories and Mathematical Models**

by

**Muhammad Tanvir Afzal (ed.)**-

**InTech**

The book is a blend of a number of great ideas, theories, mathematical models, and practical systems in the domain of Semantics. Topics include: Background; Queries, Predicates, and Semantic Cache; Algorithms and Logic Programming; etc.

(

**4198**views)

**Datalogi V - Programming Languages**

by

**A. Filinski, R. Gluck, N. D. Jones**-

**Datalogisk Institut**

This text concerns several dimensions of programming languages. We will emphasize precise definitions of the effects of various programming language features, the semantics and implementation of programming languages, and proofs concerning programs.

(

**4339**views)

**Lectures on the Curry-Howard Isomorphism**

by

**Morten Heine B. Sorensen, Pawel Urzyczyn**-

**Elsevier Science**

This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic.

(

**5862**views)

**Computational Category Theory**

by

**D.E. Rydeheard, R.M. Burstall**

The book is a bridge-building exercise between computer programming and category theory. Basic constructions of category theory are expressed as computer programs. It is a first attempt at connecting the abstract mathematics with concrete programs.

(

**10847**views)