The "sequel" to TypesAndProgrammingLanguages
, if you will. Whereas TAPL is a comprehensive, but generic, introduction to TypeTheory
, ATTAPL covers many advanced topics in TypeTheory
, such as LinearTypes
, dependent types (PredicateTypes
), types for low-level languages, ProofCarryingCode
, equivalence checking, module systems, TypeInference
, various typing schemes to deal with memory management, and more. The book is quite internally consistent in its notation, nomenclature, and style, unusual for an edited volume.
You should probably read TAPL (or another introduction to TypeTheory
, though TAPL is probably the best book out there on the subject) before reading this.
A great thing about that cover design is that you can spill coffee and Mountain Dew all over it, and it wouldn't look any different :-)