Programming Books C Java PHP Python Learn more Browse Programming Books

Sorry, this item is not available in
Image not available for
Image not available

To view this video download Flash Player


Sign in to turn on 1-Click ordering
Sell Us Your Item
For a $51.10 Gift Card
Trade in
Kindle Edition
Read instantly on your iPad, PC, Mac, Android tablet or Kindle Fire
Buy Price: $48.49
Rent From: $25.77
More Buying Choices
Have one to sell? Sell yours here

Types and Programming Languages [Hardcover]

Benjamin C. Pierce
4.6 out of 5 stars  See all reviews (13 customer reviews)

Buy New
$80.75 & FREE Shipping. Details
$36.95 & FREE Shipping. Details
In Stock.
Ships from and sold by Gift-wrap available.
In Stock.
Rented by RentU and Fulfilled by Amazon.
Want it Tuesday, July 15? Choose One-Day Shipping at checkout. Details
Free Two-Day Shipping for College Students with Amazon Student


Amazon Price New from Used from
Kindle Edition
Rent from
Hardcover $80.75  
Paperback --  
Shop the new
New! Introducing the, a hub for Software Developers and Architects, Networking Administrators, TPMs, and other technology professionals to find highly-rated and highly-relevant career resources. Shop books on programming and big data, or read this week's blog posts by authors and thought-leaders in the tech industry. > Shop now

Book Description

February 1, 2002 0262162091 978-0262162098 1

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 software engineering, language design, high-performance compilers, and security.This text provides a comprehensive introduction both to type systems in computer science and to the basic theory of programming languages. The approach is pragmatic and operational; each new concept is motivated by programming examples and the more theoretical sections are driven by the needs of implementations. Each chapter is accompanied by numerous exercises and solutions, as well as a running implementation, available via the Web. Dependencies between chapters are explicitly identified, allowing readers to choose a variety of paths through the material.The core topics include the untyped lambda-calculus, simple type systems, type reconstruction, universal and existential polymorphism, subtyping, bounded quantification, recursive types, kinds, and type operators. Extended case studies develop a variety of approaches to modeling the features of object-oriented languages.

Frequently Bought Together

Types and Programming Languages + Advanced Topics in Types and Programming Languages + Purely Functional Data Structures
Price for all three: $181.54

Buy the selected items together

Editorial Reviews


"Types are the leaven of computer programming; they make it digestible. This excellent book uses types to navigate the rich variety of programming languages, bringing a new kind of unity to their usage, theory, and implementation. Its author writes with the authority of experience in all three of these aspects." Robin Milner, Computer Laboratory, University of Cambridge

"Written by an outstanding researcher, this book is well organized and very clear, spanning both theory and implementation techniques, and reflecting considerable experience in teaching and expertise in the subject."--John Reynolds, School of Computer Science, Carnegie Mellon University

"Types are the leaven of computer programming; they make it digestible. This excellent book uses types to navigate the rich variety of programming languages, bringing a new kind of unity to their usage, theory, and implementation. Its author writes with the authority of experience in all three of these aspects."--Robin Milner, Computer Laboratory, University of Cambridge

"Types and Programming Languages is carefully written with a well-balanced choice of topics. It focusses on pragmatics, with the right level of necessary theory. The exercises in this book range from easy to challenging and provide stimulating material for beginning and advanced readers, both programmers and the more theoretically minded."--Henk Barendregt, Faculty of Science, Mathematics, and Computer Science, University of Nijmegen, The Netherlands

"Over the last two decades type theory has emerged as the central, unifying framework for research in programming languages. But these remarkable advances are not as well-known as they should be. The rapid advance of research on type systems for programming languages has far outpaced its dissemination to the rest of the field. No more. Pierce's book not only provides a comprehensive account of types for programming languages, but it does so in an engagingly elegant and concrete style that places equal emphasis on theoretical foundations and the practical problems of programming. This book will be the definitive reference for many years to come."--Robert Harper, Professor, Computer Science Department, Carnegie Mellon UniversityPlease note: Endorser gives permission to use the final two sentences of the quote as his endorsement, if necessary.

About the Author

Benjamin C. Pierce is Professor of Computer and Information Science at the University of Pennsylvania.

Product Details

  • Hardcover: 645 pages
  • Publisher: The MIT Press; 1 edition (February 1, 2002)
  • Language: English
  • ISBN-10: 0262162091
  • ISBN-13: 978-0262162098
  • Product Dimensions: 9.4 x 8.3 x 1.6 inches
  • Shipping Weight: 2.9 pounds (View shipping rates and policies)
  • Average Customer Review: 4.6 out of 5 stars  See all reviews (13 customer reviews)
  • Amazon Best Sellers Rank: #180,624 in Books (See Top 100 in Books)

More About the Author

Discover books, learn about writers, read author blogs, and more.

Customer Reviews

Most Helpful Customer Reviews
53 of 57 people found the following review helpful
5.0 out of 5 stars An accessible yet thorough introduction to type systems December 29, 2002
This text is perhaps the most accessible yet thorough introduction to type systems I've encountered.
On the one hand, it offers excellent grounding: practical motivation is provided, numerous examples illustrate the concepts, and implementations are provided which can be used to typecheck and evaluate these examples. At various points, extended demonstrations of the type systems under consideration are given (e.g. showing how objects may be encoded). The exercises are well constructed and in many cases, accompanied with answers and detailed explanations in the appendix.
On the other hand, it offers an excellent exposition of the material: Pierce provides a lucid account of the static and dynamic semantics (primarily small-step operational) for various lambda calculi. He proceeds in a stepwise fashion via the gradual accretion of features: from first order (simply typed) systems to higher order systems incorporating bounded subtyping and recursion. He also gives attention to the metatheory of these systems (focusing on proofs of progress and preservation, and for systems with subtyping, of decideability). Internally, the text is well organized, with clear dependencies among the chapters, and the bibliography is extensive.
It should be noted that, while reasonably comprehensive, the text is necessarily limited in scope. For example, aside from the discussion on Featherweight Java, systems other than typed lambda calculus variants are not considered. In my opinion, the focus on these (in some sense "low-level") calculi makes foundational issues more apparent, and the linear progression from simple to complex variants lends a pleasant cohesiveness that would have been lost in a more general survey. However, as object/class encodings were discussed at various points, it would have been nice to see a more integrated presentation, in the spirit of the paper Comparing Object Encodings [BCP97].
Comment | 
Was this review helpful to you?
26 of 26 people found the following review helpful
5.0 out of 5 stars Just right June 3, 2007
This is a textbook about programming language theory, somewhat mathematical-- but it's must-read material for anyone who wants to gripe about programming languages cluefully, much less design them.

For me, this book strikes exactly the right balance between theory and practicality. Chapters on the mathematical properties of various tiny programming languages are interleaved with chapters that provide annotated implementations of those languages.

The book will also give you the background (notation and terminology) you'll need to read cutting-edge research papers on programming language theory.

This book contains all the information I was missing. Excellent presentation of the material, well written, great exercises, doesn't go off into lala-land. Highly recommended. Some math background very helpful (you need to know what a mathematical proof is).
Was this review helpful to you?
13 of 13 people found the following review helpful
5.0 out of 5 stars Excellent book April 6, 2008
By agentzh
Writing baby interpreters using OCaml for the funny languages (include lambda calculus!) used in the theoretic chapters is a pretty cool idea and I really like it.

Elementary discrete mathematics and first-order logic are required for grokking the maths materials through out the book though. If you don't have enough patience to deal with math symbols, theorems, and formal proving, then this is not the right book for you ;)

IHMO, this is a highly comprehensible book for introducing lambda-calculus and type theory to readers without much background knowledge in either abstract algebra or theoretic computer science (like me ;)). I've been looking for such a book for long, in fact :)

Besides, this was the very book which directly inspired the birth of Pugs (a Perl 6 interpreter/compiler in Haskell) according to Audrey, the Pugs project's leader.

Highly recommended!
Comment | 
Was this review helpful to you?
18 of 21 people found the following review helpful
5.0 out of 5 stars Well put, practical and theoretic book on types. December 21, 2004
Extremely well written book on type systems in programming languages. Uses lambda calculus to explain type systems. Practical aspects show up in the ML implementations downloadable on the books site.

Contains a lot of programming language theory besides just type-systems. Can be used as an introductionary book to programming language design. Concluding: Great book!
Comment | 
Was this review helpful to you?
3 of 3 people found the following review helpful
5.0 out of 5 stars One of the best PL books January 7, 2013
Format:Hardcover|Verified Purchase
This books is a good introduction to programming languages through type systems. The book has very pedagogical structure which makes it easy to read even for people who didn't have a good PL or mathematical background. There are a large number of examples, and exercises with answers which make it easy to check that you understand the book correctly.

However, there are several problems:
- first the book uses OCaml which isn't in wide use today.
- proofs in the last chapters looks like they are copy-pasted from a proof assistant like Coq and are very hard to read and comprehend (not because they are intricate and complex but because of their gigantic size).

P.S. I recommend everyone who reads this book another online material by Benjamin Pierce: [...] It contains similar content but with the aim of using Coq for all the theory.
Comment | 
Was this review helpful to you?
46 of 68 people found the following review helpful
4.0 out of 5 stars Not quite what I was looking for June 12, 2005
Format:Hardcover|Verified Purchase
I need basic information on type safety, theory of object oriented typing, and how to axiomatize nonstandard kind of typing systems. I need it now, in a form that I can put to use without too many side trips

This book is almost what I was looking for. It builds up a semantic logic based on lambda calculus, then creates typed versions. Pierce really does work very methodically up through the levels, ending at about the place where C++ templates and recursive type definitions start. Along the way, he's careful to match the typing axioms to semantics, covering unusual topics like exceptions and type inference while he's at it.

Almost what I was looking for, but not quite. As I said, I have immediate needs, and I'm not into theory for its own sweet sake. That means I had little appreciation for all the chapters that created arithmetic all over again, starting from Peano axioms (or something like), via the lambda calculus. I know that low-level axiomatizations and lambda calculus are much beloved of the theoreticians, but I encounter them only rarely, and when I was trying to get something else done, like now. For me, they created a diversion blocked by an impediment. Also, however convenient it may be for theory, functional programming is mostly a journal-page peculiarity in industrial practice. I admit, analysis of functional programs pushed me into insight I might have missed, but I would probably have been quite happy dealing with assignment formalisms instead.

I almost gave this three stars, because its unnecessary notational baggage and off-main-stream topics weren't doing my job. Bruce's book (ISBN 026202523X) was a much more profitable use of my time. Still, Pierce's goals weren't mine, and the mansion of type analysis has many rooms. Not all of those rooms are furnished to my taste, and don't need to be. I rounded up to four stars for what it meant to do.

Comment | 
Was this review helpful to you?
Most Recent Customer Reviews
2.0 out of 5 stars Awesome book screwed up by terrible translation to electronic format
Pierce's book is a classic. Unfortunately, this particular version of it is outright horrible. It pretty much reproduces the format of an actual paper book, preserving the page... Read more
Published 29 days ago by P. Lepin
5.0 out of 5 stars A must-buy
Fantastic introduction, very readable. I bought it a few years ago and I still reference it time and time again.
Published 8 months ago by Wojciech Jedynak
5.0 out of 5 stars Very clear
This book explains what you would expect from title in a clear, understandable way for those who are not familiar with programming language theory. Read more
Published 8 months ago by Shigeo Nishi
5.0 out of 5 stars PL enthusiasts should start here
This is a great book. Benjamin's style is fairly conversational keeping this very dry and logical topic fresh and inviting. Read more
Published 9 months ago by Zac Slade
5.0 out of 5 stars An excellent step-by-step guide from simple types and languages to...
In my opinion the best written and most effective introduction to type theory and programming languages. Read more
Published 16 months ago by John Nash
4.0 out of 5 stars The best book on the subject.
This book is the best book on the subject, as far as I can find. My only complaint is that a lot of the syntax of the language denotation is unsystematic, and a lot of new... Read more
Published on February 22, 2011 by T. Schaeffer
5.0 out of 5 stars A Good Book
Especially helpful for those who have practical experience but don't have strong theoretical background (like Lambda Calculus, Typing Theory ... etc.)
Published on September 25, 2002 by "hongjiang"
Search Customer Reviews
Search these reviews only

What Other Items Do Customers Buy After Viewing This Item?


There are no discussions about this product yet.
Be the first to discuss this product with the community.
Start a new discussion
First post:
Prompts for sign-in

Look for Similar Items by Category