We have been using this book on a course in programming language foundations - and I strongly recommend it.
It is well written, the proofs are well explained and detailed (at least in the beginning - later on he assumes that we are adept at structural induction), the exercises are very helpful, and the insights provided regarding evaluation semantics and type safety are delightful. In the first 11 chapters, the author introduces a very simple untyped language with three syntactical forms, specifies the evaluation semantics of this language, then introduces a pure lambda calculus and does the same (also shows us how to do recursion in a pure lambda calculus! - this is kool because lambdas don't really have names), then combines the two languages, then adds types to these languages and shows us what type safety is and how we can prove it. He also shows how to add extensions (let, records, sequencing) to our simple lambda calculus while proving type safety. We are midway through the chapter on adding references to our lambda calculus, and if i may repeat myself, the book is a delightful read. (I am especially looking forward to the section that shows how to prove type safety in a language that allows subtyping) I can't imagine someone with your interests not enjoying this book ;-) regards, Faisal Vali David Abrahams wrote: > > While I was in Oxford I happened to pick up a copy of this book at > Blackwell's (the greatest bookstore in all of England): > http://www.cis.upenn.edu/~bcpierce/tapl/ > > It seemed like a beautifully understandable tour of type theory and > its application in real programming languages. It even had a section > on Jeremy's latest obsession: existential types. Does anyone else > have experience with this book? I'm planning to buy it unless > someone can tell me that they know of a better one. > > -- > Dave Abrahams > Boost Consulting > www.boost-consulting.com > > _______________________________________________ > Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost _______________________________________________ Unsubscribe & other changes: http://lists.boost.org/mailman/listinfo.cgi/boost