Goodreads helps you keep track of books you want to read.

Start by marking “Types and Programming Languages” as Want to Read:

Other editions

Enlarge cover

Rate this book

Clear rating

1 of 5 stars 2 of 5 stars 3 of 5 stars 4 of 5 stars 5 of 5 stars

Open Preview

Types and Programming Languages

Benjamin C. Pierce

4.26 · Rating details · 528 ratings · 17 reviews

A comprehensive introduction to type systems and programming languages.A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to the kinds of values they compute. The study of type systems--and of programming languages from a type-theoretic perspective--has important applications in ...more

Get A Copy

Hardcover, 623 pages

Published January 4th 2002 by MIT Press (first published 2002)

More Details... Edit Details

Friend Reviews

To see what your friends thought of this book, please sign up.

Reader Q&A

To ask other readers questions about Types and Programming Languages, please sign up.

Be the first to ask a question about Types and Programming Languages

Lists with This Book

Structure and Interpretation of Computer Programs by Harold Abelson

Purely Functional Data Structures by Chris Okasaki

Types and Programming Languages by Benjamin C. Pierce

Pearls of Functional Algorithm Design by Richard S. Bird

Learn You a Haskell for Great Good! by Miran Lipovača

Functional Programming

47 books — 32 voters

Computational Complexity by Sanjeev Arora

The C Programming Language by Brian W. Kernighan

Approximation Algorithms by Vijay V. Vazirani

Theory of Computation by Dexter C. Kozen

Computer Science Year 4 (MCSL)

25 books — 8 voters

More lists with this book...

Community Reviews

Showing 1-30

Average rating 4.26 ·

Rating details

· 528 ratings · 17 reviews

More filters

Sort order

Start your review of Types and Programming Languages

Jul 07, 2014 Zhi Han rated it it was amazing

Shelves: programming, favorites

One of my most unpleasant experience in grad school is when I has absolutely no idea what his peers are talking about. I frequently found myself in that situation during my years at CMU. Type theory is one of the topics. Why didn’t I just ask them? I did. My friend Oliver once gave me the perfect response: “I cannot afford to spend time on educating you.” In a world full of distractions and useless information, time is very valuable resource. If one wants to learn, he has to spend his own time

Th One of my most unpleasant experience in grad school is when I has absolutely no idea what his peers are talking about. I frequently found myself in that situation during my years at CMU. Type theory is one of the topics. Why didn’t I just ask them? I did. My friend Oliver once gave me the perfect response: “I cannot afford to spend time on educating you.” In a world full of distractions and useless information, time is very valuable resource. If one wants to learn, he has to spend his own time

That is why I picked up the Benjamin Pierce’s book after many years of random embarrassments. I am glad that I did it. The book is really a fun read. And it really is nice written. Having read some technical books from both engineering and computer science categories, I have always found the computer science books more enjoyable and, in some sense, entertaining. For example, many hard core computer science books deliberately puts some effort in telling the history of the technology. And computer science people like to decorate the text with a few fun quotes. They all make the reading and learning more fun.

The book is very well written. By very well, I mean 1) it spend enough effort on the basics. It elaborates all the details and mathematical backgrounds that one need to acquire. 2) It develop the framework in a nicely slow, step-by-step pace. Every chapter is a very small enhancement over the last few chapters. And the author even takes the time to highlight the newly added rules in the type system. 3) It gives appropriate references for further reading. I did not check the references, but from the text it sure looks appropriate and thorough. 4) It has all the details of the proof, if one prefer, he/she can check the proofs themselves.

I like the book mainly because it makes me appreciate the type system. I remember the frustration that I had when I was writing some C++ template program. Not to mention the times that I was scratching my head over some weird OCaml type errors. A year ago I was fully convinced type checking is a complete pain in the butt; it slows us developers down and we should all write in Python, Ruby or MATLAB. But now I changed my mind. When Herb Sutter says ‘type system is your friend’ on channel 9, I tend to agree with him. ...more

flag 16 likes · Like · see review

Jan 12, 2010 Leo Horovitz rated it really liked it

Shelves: science, formal-science, formal-language, computer-science, lambda-calculus, programming-languages, programming-language-theory, type-theory, non-fiction

After spending years on my shelf and having been partially read at least once before, this book was finally finished! (I don't know why I used the passive form there, it just felt right for some reason)

I'm glad I did finally read it, even though there were parts that were glanced through without too much attention to detail and even though I skipped the exercises that are probably needed to get a more thorough understanding of the material. I read it mostly as a way to get a good overview of the After spending years on my shelf and having been partially read at least once before, this book was finally finished! (I don't know why I used the passive form there, it just felt right for some reason)

I'm glad I did finally read it, even though there were parts that were glanced through without too much attention to detail and even though I skipped the exercises that are probably needed to get a more thorough understanding of the material. I read it mostly as a way to get a good overview of the basics of typed lambda calculi, which the book supplies with a focus on the use of such formalism in the specification and analysis of programming languages. The book is divided into six major parts which all deal with increasing levels of complexity in type systems. The first part introduces untyped formal calculi, first simple arithmetic expressions, then the classic lambda calculus. After this follows a part of simply typed lambda calculi which begins with nothing but function types and later expands this with base types and different structured types such as pairs, tuples, records, lists and other common forms of types. The next major part deals with subtyping and how it interacts with the forms of types presented so far, and after that there's a part of recursive types. While the expansions to the simply typed lambda calculus introduced so far have lots of interesting uses as well as theoretical properties, neither of them introduces something really new in the expressiveness of the language, at least nothing as important as the polymorphism introduced in part five. The reason I value this so much higher is that it enables a completely new form of abstraction. All the systems introduces before this have only the basic function abstraction on the level of terms, but with polymorphism, the ability to abstract over types in terms is introduced (the first step to move away from the first corner of the Barendregt, or lambda, cube which we will talk more about soon). Polymorphism through both universal and existential quantification is presented in different forms and at the end of the part, polymorphism is combined with subtyping in a non-trivial way yielding bounded quantification. Finally, the book is ended with a short part on higher-order systems featuring type operators and kinding (a way to classify the level of types in terms of kinds in the same way that term-level expressions are classified by types) constituting another move in the Barendregt cube where we can now abstract over types in type expressions. The final move possible in the cube, yielding dependent types (abstraction over term-level expressions in types) is also briefly mentioned but not worked out formally as the rest are.

The Barendregt cube is a unifying way to look at the expressiveness possible in the different type systems presented here and elsewhere, and another interesting and unifying theme is that of the Curry-Howard isomorphism, stating that there is a correspondence between programs and proofs on the one hand and types and propositions on the other so that a program having a certain type in a formal calculus corresponds to a proof of a corresponding proposition in a logic. This is discussed at many point throughout the book, giving historical explanations of how the correspondence between specific logics and corresponding type systems have been invented/discovered (depending on your particaular view on philosophy of mathematics and/or logic).

It's a fairly theoretical text, but with many examples, the type systems are not presented as pure formalisms but are motivated through code examples in the calculi presented and at three different points in the book, attempts at formalizing object-oriented concepts in the calculi are presented with increasing sophistication as the new expressive power of the formalisms developed allows it.

As an overview of the formal specifications of programming languages, their syntax and semantics (with a special focus on type systems), along with practical motivations, some points on implementations (almost all the formalisms introduced have actual accompanying implementations to be downloaded from the book's website), proofs of metatheoretic properties and comparisons with some actual programming languages, the book could hardly be better. The only reason that I'm not giving it five stars is that I reserve that for books that are almost perfect, and this does not quite live up to such a high standard. For example, the sometimes very technical proofs are a bit too dense for my taste. Towards the end of the book, there are some attempts at giving a more intuitive sense for some of the formalisations by presenting some of the mechanisms in an anthropomorphic way, by describing a function as saying something along the lines of "give me a value of such and such type, along with a function... and I will apply the function to produce a result..." which I appreciated highly. Had the whole book attempted to present things in such a manner more, had the author stopped now and then to discuss things in a more intuitive way, then I probably would have given it five stars. As it is though, it's an excellent book that I highly recommend for anyone interested in the subject. ...more

flag 7 likes · Like · see review

Aug 29, 2007 Steve rated it really liked it

I liked the structure: starting simple, explaining things clearly, and building slowly.

Don't attempt to read this book without at least a basic knowledge of doing proofs in math and higher-order logic. This should cover you: Language, Proof and Logic: Text and CD

As you work on implementing your own type systems, you'll find the detailed metatheory chapters worth revisiting.
...more

flag 4 likes · Like · see review

May 17, 2007 Sam marked it as to-read

Recommends it for: Any programmer interested in writing their own programming language(s)

Perhaps the best book of its kind for the beginning/intermediate programmer interested in PLT (programming language theory). The book covers the simple untyped lambda calculus and builds on that foundation to many typed lambda calculi. Implementation chapters show the reader how to put the information to good use, providing executable code in the O'Caml language.

As a non-mathematician, programming hobbyist without formal experience or training, I've found this book particularly helpful in follow ...more

flag 2 likes · Like · see review

Dec 19, 2015 Sandy Vanderbleek rated it it was amazing

It's awesome. Personally sub-typing and implementing Java wasn't interesting to me but everything else was. ...more

flag 1 like · Like · see review

Oct 21, 2017 Michel Beloshitsky rated it it was amazing

Very good introduction into theory of types. Useful if your dealing with modern software development tools, like Kotlin, Facebook's Flow, Haskell, Typescript.
...more

flag Like · see review

Jul 26, 2017 Damir rated it really liked it

This review has been hidden because it contains spoilers. To view it, click here.

flag Like · see review

Aug 26, 2008 Eric Walkingshaw rated it it was amazing

Shelves: science

An invaluable reference for programming language theory. Especially useful for those interested in functional languages, which seem to be poorly covered elsewhere. This book works in the opposite direction as most, assuming a functional approach and eventually deriving imperative constructs, rather than the other way around. I like this much better, but it may be tough if you lack the functional background.

One thing I've noticed is that people seem to get hung up over the notation and liberal u ...more

flag Like · see review

Feb 12, 2012 Mark added it

Shelves: to-reread, tech-queue, tech-formal

Excellent. A small note: if (like me) you get bogged down in the proofs, Pierce's Software Foundations may be a better introduction to ideas such as type preservation, progress properties, and induction over terms and type derivations. I wish I'd read that work first. ...more

flag Like · see review

Oct 01, 2016 jg rated it it was amazing

Very clear & accessible intro to programming language theory. Lots of late-night fun to be had here.

Make sure you check out the OCaml code that accompanies it. It provides just enough motivation & examples to keep going through the theory in the actual text.

flag Like · see review

Aug 09, 2013 Scott Wisniewski rated it it was amazing

Awesome book, particularly if you like programming languages.

Also, the proof exercises are good at training your brain for combinatorial reasoning. It helps to makes reasoning about programing languages intuitive.

I loved this book.

flag Like · see review

Mar 05, 2009 Andrew rated it liked it

A classic in Type Theory, it gives you background in something modern programmers are woefully and shamefully ignorant in.

flag Like · see review

Mar 17, 2014 Jyri-Matti Lähteenmäki rated it really liked it

Shelves: dev

I doubt that I would have gotten total understanding even if I hade made the exercises, but still, I got a lot of understanding about type systems and the kind of things there are to consider.

flag Like · see review