Truck Month Textbook Trade In Amazon Fashion Learn more Discover it Lacuna Coil Father's Day Gift Guide 2016 Fire TV Stick The Baby Store Find the Best Purina Pro Plan for Your Pet Amazon Cash Back Offer DrThorne DrThorne DrThorne  Amazon Echo  Echo Dot  Amazon Tap  Echo Dot  Amazon Tap  Amazon Echo Introducing new colors All-New Kindle Oasis AutoRip in CDs & Vinyl Outdoor Recreation

Customer Reviews

4.6 out of 5 stars19
Format: Hardcover|Change
Price:$83.99+ Free shipping with Amazon Prime
Your rating(Clear)Rate this item


There was a problem filtering reviews right now. Please try again later.

on 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].
0Comment|56 people found this helpful. Was this review helpful to you?YesNoReport abuse
on 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).
11 comment|28 people found this helpful. Was this review helpful to you?YesNoReport abuse
on June 14, 2014
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 layout, and sells it as a "feature"... What this means in practice is that it's barely readable on mobile devices, and the smaller the screen the worse it is. If you're vision impaired to boot, just forget about it. To add insult to the injury, you can't read it on Kindle Cloud Reader, for some inexplicable reason.

The book is absolutely great. But I regretted buying this particular version of it.
0Comment|23 people found this helpful. Was this review helpful to you?YesNoReport abuse
on April 6, 2008
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!
0Comment|14 people found this helpful. Was this review helpful to you?YesNoReport abuse
on January 7, 2013
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.
0Comment|7 people found this helpful. Was this review helpful to you?YesNoReport abuse
on 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!
0Comment|20 people found this helpful. Was this review helpful to you?YesNoReport abuse
on August 17, 2014
Awesome book but the Kindle version is unreadable, one third of the screen is margin. Have fun zooming in and out. Also for some inexplicable reason this kindle book is not available to read on kindle for android on my phone!! (with the error message: "this item is not compatible with this device) I guess they figured since they wasted half the screen space with margins they might add as a minimum requirement a big tablet screen, otherwise refuse to display the book. Neither on the cloud reader.
0Comment|7 people found this helpful. Was this review helpful to you?YesNoReport abuse
on March 1, 2013
In my opinion the best written and most effective introduction to type theory and programming languages. I am having fun implementing a practical functional programming language with dependent types and this book is always next to me when I code.
0Comment|3 people found this helpful. Was this review helpful to you?YesNoReport abuse
on October 15, 2013
This is a great book. Benjamin's style is fairly conversational keeping this very dry and logical topic fresh and inviting. The notation used can seem a little esoteric for the uninitiated, however there is enough detail early on to get you over this hurdle quickly. Soon you will be writing your own substitutions, elimination rules and type judgements needed for any programming language you might want to design.
0Comment|2 people found this helpful. Was this review helpful to you?YesNoReport abuse
on September 27, 2015
Published in 2002, *Types and Programming Languages* is now a classic of computer science: in it Penn's Benjamin Pierce did what many CS writers fail to do by systematically breaking down a particular part of the programming language world to techdom's enduring benefit. The book does not talk about every little topic it could, but its well-organized approach to static type systems carries the reader far with only the necessary effort. Simply put, the text is devoted to giving operational semantics for richer and richer variants of the simply typed lambda calculus, that logical formalism for computation which has an extremely close likeness to functional programming languages and more than a "family resemblance" to imperative ones. The operational approach to computer language semantics used here is akin to giving introduction and elimination rules for logical operators, long the favored way to teach undergraduates symbolic logic; in contrast to denotational semantics, it proves to be both flexible and "close to the machine".

Starting out with the basic principles behind type systems for programming languages and an easy-to-follow introduction to lambda calculus, Pierce gradually adds more sophisticated features ("built-in" data types, mutable references, polymorphism, "subtyping" necessary for object-oriented programming, the quantification over types of Girard's System F) and explores their connection to practical languages using OCaml programs that easily translate the ideas into code. The logically sophisticated will note that as these systems grow in expressive power, the nice features like computational tractability understandably bleed away -- however, the author was obviously not out to write a compiler textbook; theoreticians and practitioners alike will learn what they need to learn about types from this book, which takes you up to readiness to read the current literature on the topic.

This is not quite an MSCE certification manual, but if you like the idea of computing you'll love having this very big part of it explained clearly and exhaustively. Pierce has a more soup-to-nuts approach to PL theory in the works, a text called *Software Foundations* (currently available online) that explains similar ideas in the idiom of the theorem prover Coq, but this isn't outdated yet; if you're tasked with reading it, get ready to get enlightened.
0Comment|Was this review helpful to you?YesNoReport abuse