[boost] Re: Types and Programming Languages

From: faisal vali (fvali_at_[hidden])
Date: 2003-04-17 14:16:29

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