Types and Programming Languages

摘要: A type system is a syntactic method for automatically checking the absence of certain erroneous behaviors by classifying program phrases according to kinds values they compute. The study systems -- and programming languages from type-theoretic perspective has important applications in software engineering, language design, high-performance compilers, security.This text provides comprehensive introduction both computer science basic theory languages. approach pragmatic operational; each new concept motivated examples more theoretical sections are driven needs implementations. Each chapter accompanied numerous exercises solutions, as well running implementation, available via Web. Dependencies between chapters explicitly identified, allowing readers choose variety paths through material.The core topics include untyped lambda-calculus, simple systems, reconstruction, universal existential polymorphism, subtyping, bounded quantification, recursive types, kinds, operators. Extended case studies develop approaches modeling features object-oriented